Theorem stoweidlem27 46018

Description: This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t₀) = 0, and p > 0 on T - U. Here (𝑞‘𝑖) is used to represent p_(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

Hypotheses

Ref	Expression
stoweidlem27.1	⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
stoweidlem27.2	⊢ (𝜑 → 𝑄 ∈ V)
stoweidlem27.3	⊢ (𝜑 → 𝑀 ∈ ℕ)
stoweidlem27.4	⊢ (𝜑 → 𝑌 Fn ran 𝐺)
stoweidlem27.5	⊢ (𝜑 → ran 𝐺 ∈ V)
stoweidlem27.6	⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙)
stoweidlem27.7	⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
stoweidlem27.8	⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋)
stoweidlem27.9	⊢ Ⅎ𝑡𝜑
stoweidlem27.10	⊢ Ⅎ𝑤𝜑
stoweidlem27.11	⊢ Ⅎℎ𝑄

Assertion

Ref	Expression
stoweidlem27	⊢ (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))))

Distinct variable groups:   ℎ,𝑖,𝑡,𝑤,𝐹   ℎ,𝑙,𝑌,𝑡,𝑤   𝑇,ℎ,𝑤   𝑖,𝑞,𝑡,𝐹   𝑖,𝐺   𝑖,𝑀,𝑞   𝑖,𝑋,𝑤   𝑖,𝑌,𝑞   𝜑,𝑖   𝑄,𝑙   𝜑,𝑙   𝐺,𝑙   𝑄,𝑞   𝑇,𝑞   𝑈,𝑞   𝑤,𝑀   𝑤,𝑄   𝑤,𝑈

Allowed substitution hints:   𝜑(𝑤,𝑡,ℎ,𝑞)   𝑄(𝑡,ℎ,𝑖)   𝑇(𝑡,𝑖,𝑙)   𝑈(𝑡,ℎ,𝑖,𝑙)   𝐹(𝑙)   𝐺(𝑤,𝑡,ℎ,𝑞)   𝑀(𝑡,ℎ,𝑙)   𝑋(𝑡,ℎ,𝑞,𝑙)

Proof of Theorem stoweidlem27

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		stoweidlem27.4	. . . 4 ⊢ (𝜑 → 𝑌 Fn ran 𝐺)
2		stoweidlem27.5	. . . 4 ⊢ (𝜑 → ran 𝐺 ∈ V)
3		fnex 7173	. . . 4 ⊢ ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V)
4	1, 2, 3	syl2anc 584	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
5		stoweidlem27.7	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
6		f1ofn 6783	. . . . 5 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹 Fn (1...𝑀))
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 Fn (1...𝑀))
8		ovex 7402	. . . 4 ⊢ (1...𝑀) ∈ V
9		fnex 7173	. . . 4 ⊢ ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
10	7, 8, 9	sylancl 586	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
11		coexg 7885	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌 ∘ 𝐹) ∈ V)
12	4, 10, 11	syl2anc 584	. 2 ⊢ (𝜑 → (𝑌 ∘ 𝐹) ∈ V)
13		stoweidlem27.3	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		f1of 6782	. . . . . 6 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)⟶ran 𝐺)
15	5, 14	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶ran 𝐺)
16		fnfco 6707	. . . . 5 ⊢ ((𝑌 Fn ran 𝐺 ∧ 𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌 ∘ 𝐹) Fn (1...𝑀))
17	1, 15, 16	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝐹) Fn (1...𝑀))
18		rncoss 5928	. . . . 5 ⊢ ran (𝑌 ∘ 𝐹) ⊆ ran 𝑌
19		fvelrnb 6903	. . . . . . . . . . 11 ⊢ (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
20	1, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
21	20	biimpa 476	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘)
22		stoweidlem27.10	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤𝜑
23		stoweidlem27.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
24		nfmpt1 5201	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
25	23, 24	nfcxfr 2889	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤𝐺
26	25	nfrn 5905	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑤ran 𝐺
27	26	nfcri 2883	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤 𝑙 ∈ ran 𝐺
28	22, 27	nfan 1899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑙 ∈ ran 𝐺)
29		stoweidlem27.6	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙)
30	29	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑙)
31		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
32	30, 31	eleqtrd 2830	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
33		nfcv 2891	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ(𝑌‘𝑙)
34		stoweidlem27.11	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ𝑄
35		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}
36		fveq1 6839	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑌‘𝑙) → (ℎ‘𝑡) = ((𝑌‘𝑙)‘𝑡))
37	36	breq2d 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑌‘𝑙) → (0 < (ℎ‘𝑡) ↔ 0 < ((𝑌‘𝑙)‘𝑡)))
38	37	rabbidv 3410	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑌‘𝑙) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)})
39	38	eqeq2d 2740	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑌‘𝑙) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
40	33, 34, 35, 39	elrabf 3652	. . . . . . . . . . . . . . 15 ⊢ ((𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
41	32, 40	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
42	41	simpld 494	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑄)
43		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺)
44	23	elrnmpt 5911	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
45	43, 44	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
46	43, 45	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
47	28, 42, 46	r19.29af 3244	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
48	47	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
49		eleq1 2816	. . . . . . . . . . 11 ⊢ ((𝑌‘𝑙) = 𝑘 → ((𝑌‘𝑙) ∈ 𝑄 ↔ 𝑘 ∈ 𝑄))
50	48, 49	syl5ibcom 245	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌‘𝑙) = 𝑘 → 𝑘 ∈ 𝑄))
51	50	reximdva 3146	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘 → ∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄))
52	21, 51	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄)
53		idd 24	. . . . . . . . . 10 ⊢ (𝑙 ∈ ran 𝐺 → (𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄))
54	53	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (𝑙 ∈ ran 𝐺 → (𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄)))
55	54	rexlimdv 3132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄))
56	52, 55	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → 𝑘 ∈ 𝑄)
57	56	ex 412	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 → 𝑘 ∈ 𝑄))
58	57	ssrdv 3949	. . . . 5 ⊢ (𝜑 → ran 𝑌 ⊆ 𝑄)
59	18, 58	sstrid 3955	. . . 4 ⊢ (𝜑 → ran (𝑌 ∘ 𝐹) ⊆ 𝑄)
60		df-f 6503	. . . 4 ⊢ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌 ∘ 𝐹) Fn (1...𝑀) ∧ ran (𝑌 ∘ 𝐹) ⊆ 𝑄))
61	17, 59, 60	sylanbrc 583	. . 3 ⊢ (𝜑 → (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄)
62		stoweidlem27.9	. . . 4 ⊢ Ⅎ𝑡𝜑
63		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑤 𝑡 ∈ (𝑇 ∖ 𝑈)
64	22, 63	nfan 1899	. . . . . 6 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈))
65		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑤∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)
66		stoweidlem27.8	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋)
67	66	sselda 3943	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 𝑡 ∈ ∪ 𝑋)
68		eluni 4870	. . . . . . 7 ⊢ (𝑡 ∈ ∪ 𝑋 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
69	67, 68	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
70	23	funmpt2 6539	. . . . . . . . . . . 12 ⊢ Fun 𝐺
71	23	dmeqi 5858	. . . . . . . . . . . . . . 15 ⊢ dom 𝐺 = dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
72		stoweidlem27.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑄 ∈ V)
73	34	rabexgf 45011	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
75	74	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
76	75	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ 𝑋 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V))
77	22, 76	ralrimi 3233	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
78		dmmptg 6203	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
79	77, 78	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
80	71, 79	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑋)
81	80	eleq2d 2814	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ dom 𝐺 ↔ 𝑤 ∈ 𝑋))
82	81	biimpar 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ dom 𝐺)
83		fvelrn 7030	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝑤 ∈ dom 𝐺) → (𝐺‘𝑤) ∈ ran 𝐺)
84	70, 82, 83	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) ∈ ran 𝐺)
85	84	adantrl 716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (𝐺‘𝑤) ∈ ran 𝐺)
86	15	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝐹:(1...𝑀)⟶ran 𝐺)
87		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝑖 ∈ (1...𝑀))
88		fvco3 6942	. . . . . . . . . . . . . 14 ⊢ ((𝐹:(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
89	86, 87, 88	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
90		fveq2 6840	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑖) = (𝐺‘𝑤) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
91	90	ad2antll 729	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
92	89, 91	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐺‘𝑤)))
93		eleq1 2816	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
94	93	anbi2d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝜑 ∧ 𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺)))
95		eleq2 2817	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘𝑙) ∈ (𝐺‘𝑤)))
96		fveq2 6840	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑌‘𝑙) = (𝑌‘(𝐺‘𝑤)))
97	96	eleq1d 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ (𝐺‘𝑤) ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
98	95, 97	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
99	94, 98	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (𝐺‘𝑤) → (((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))))
100	99, 29	vtoclg 3517	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
101	100	anabsi7 671	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
102	101	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
103	92, 102	eqeltrd 2828	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
104		f1ofo 6789	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)–onto→ran 𝐺)
105		forn 6757	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺)
106	5, 104, 105	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 = ran 𝐺)
107	106	eleq2d 2814	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
108	107	biimpar 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝐺‘𝑤) ∈ ran 𝐹)
109	7	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀))
110		fvelrnb 6903	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn (1...𝑀) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
111	109, 110	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
112	108, 111	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤))
113	103, 112	reximddv 3149	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
114	85, 113	syldan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
115		simplrl 776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ 𝑤)
116		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑋)
117	23	fvmpt2 6961	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ 𝑋 ∧ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
118	116, 75, 117	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
119	118	eleq2d 2814	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) ↔ ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
120	119	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
121	120	adantlrl 720	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
122		nfcv 2891	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ((𝑌 ∘ 𝐹)‘𝑖)
123		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}
124		fveq1 6839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (ℎ‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
125	124	breq2d 5114	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (0 < (ℎ‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
126	125	rabbidv 3410	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
127	126	eqeq2d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
128	122, 34, 123, 127	elrabf 3652	. . . . . . . . . . . . . . . 16 ⊢ (((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
129	121, 128	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
130	129	simprd 495	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
131	115, 130	eleqtrd 2830	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
132		rabid 3424	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
133	131, 132	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
134	133	simprd 495	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
135	134	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
136	135	reximdv 3148	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
137	114, 136	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
138	137	ex 412	. . . . . . 7 ⊢ (𝜑 → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
139	138	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
140	64, 65, 69, 139	exlimimdd 2220	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
141	140	ex 412	. . . 4 ⊢ (𝜑 → (𝑡 ∈ (𝑇 ∖ 𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
142	62, 141	ralrimi 3233	. . 3 ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
143	13, 61, 142	jca32 515	. 2 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))))
144		feq1 6648	. . . . 5 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄))
145		fveq1 6839	. . . . . . . . 9 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞‘𝑖) = ((𝑌 ∘ 𝐹)‘𝑖))
146	145	fveq1d 6842	. . . . . . . 8 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞‘𝑖)‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
147	146	breq2d 5114	. . . . . . 7 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (0 < ((𝑞‘𝑖)‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
148	147	rexbidv 3157	. . . . . 6 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
149	148	ralbidv 3156	. . . . 5 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
150	144, 149	anbi12d 632	. . . 4 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)) ↔ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))))
151	150	anbi2d 630	. . 3 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))) ↔ (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))))
152	151	spcegv 3560	. 2 ⊢ ((𝑌 ∘ 𝐹) ∈ V → ((𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)))))
153	12, 143, 152	sylc 65	1 ⊢ (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876  ∀wral 3044  ∃wrex 3053  {crab 3402  Vcvv 3444   ∖ cdif 3908   ⊆ wss 3911  ∪ cuni 4867   class class class wbr 5102   ↦ cmpt 5183  dom cdm 5631  ran crn 5632   ∘ ccom 5635  Fun wfun 6493   Fn wfn 6494  ⟶wf 6495  –onto→wfo 6497  –1-1-onto→wf1o 6498  ‘cfv 6499  (class class class)co 7369  0cc0 11044  1c1 11045   < clt 11184  ℕcn 12162  ...cfz 13444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372

This theorem is referenced by:  stoweidlem35  46026