Theorem stoweidlem27 41749

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) = 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 6806	. . . 4 ⊢ ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V)
4	1, 2, 3	syl2anc 576	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
5		stoweidlem27.7	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
6		f1ofn 6445	. . . . 5 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹 Fn (1...𝑀))
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 Fn (1...𝑀))
8		ovex 7008	. . . 4 ⊢ (1...𝑀) ∈ V
9		fnex 6806	. . . 4 ⊢ ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
10	7, 8, 9	sylancl 577	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
11		coexg 7449	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌 ∘ 𝐹) ∈ V)
12	4, 10, 11	syl2anc 576	. 2 ⊢ (𝜑 → (𝑌 ∘ 𝐹) ∈ V)
13		stoweidlem27.3	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		f1of 6444	. . . . . 6 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)⟶ran 𝐺)
15	5, 14	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶ran 𝐺)
16		fnfco 6372	. . . . 5 ⊢ ((𝑌 Fn ran 𝐺 ∧ 𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌 ∘ 𝐹) Fn (1...𝑀))
17	1, 15, 16	syl2anc 576	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝐹) Fn (1...𝑀))
18		rncoss 5685	. . . . 5 ⊢ ran (𝑌 ∘ 𝐹) ⊆ ran 𝑌
19		fvelrnb 6556	. . . . . . . . . . 11 ⊢ (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
20	1, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
21	20	biimpa 469	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘)
22		stoweidlem27.10	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤𝜑
23		stoweidlem27.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
24		nfmpt1 5025	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
25	23, 24	nfcxfr 2930	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤𝐺
26	25	nfrn 5667	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑤ran 𝐺
27	26	nfcri 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤 𝑙 ∈ ran 𝐺
28	22, 27	nfan 1862	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑙 ∈ ran 𝐺)
29		stoweidlem27.6	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙)
30	29	ad2antrr 713	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑙)
31		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
32	30, 31	eleqtrd 2868	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
33		nfcv 2932	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ(𝑌‘𝑙)
34		stoweidlem27.11	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ𝑄
35		nfv 1873	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}
36		fveq1 6498	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑌‘𝑙) → (ℎ‘𝑡) = ((𝑌‘𝑙)‘𝑡))
37	36	breq2d 4941	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑌‘𝑙) → (0 < (ℎ‘𝑡) ↔ 0 < ((𝑌‘𝑙)‘𝑡)))
38	37	rabbidv 3403	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑌‘𝑙) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)})
39	38	eqeq2d 2788	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑌‘𝑙) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
40	33, 34, 35, 39	elrabf 3591	. . . . . . . . . . . . . . 15 ⊢ ((𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
41	32, 40	sylib 210	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
42	41	simpld 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑄)
43		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺)
44	23	elrnmpt 5671	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
45	43, 44	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
46	43, 45	mpbid 224	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
47	28, 42, 46	r19.29af 3272	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
48	47	adantlr 702	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
49		eleq1 2853	. . . . . . . . . . 11 ⊢ ((𝑌‘𝑙) = 𝑘 → ((𝑌‘𝑙) ∈ 𝑄 ↔ 𝑘 ∈ 𝑄))
50	48, 49	syl5ibcom 237	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌‘𝑙) = 𝑘 → 𝑘 ∈ 𝑄))
51	50	reximdva 3219	. . . . . . . . 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 3228	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄))
56	52, 55	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → 𝑘 ∈ 𝑄)
57	56	ex 405	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 → 𝑘 ∈ 𝑄))
58	57	ssrdv 3864	. . . . 5 ⊢ (𝜑 → ran 𝑌 ⊆ 𝑄)
59	18, 58	syl5ss 3869	. . . 4 ⊢ (𝜑 → ran (𝑌 ∘ 𝐹) ⊆ 𝑄)
60		df-f 6192	. . . 4 ⊢ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌 ∘ 𝐹) Fn (1...𝑀) ∧ ran (𝑌 ∘ 𝐹) ⊆ 𝑄))
61	17, 59, 60	sylanbrc 575	. . 3 ⊢ (𝜑 → (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄)
62		stoweidlem27.9	. . . 4 ⊢ Ⅎ𝑡𝜑
63		nfv 1873	. . . . . . 7 ⊢ Ⅎ𝑤 𝑡 ∈ (𝑇 ∖ 𝑈)
64	22, 63	nfan 1862	. . . . . 6 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈))
65		nfv 1873	. . . . . 6 ⊢ Ⅎ𝑤∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)
66		stoweidlem27.8	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋)
67	66	sselda 3858	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 𝑡 ∈ ∪ 𝑋)
68		eluni 4715	. . . . . . 7 ⊢ (𝑡 ∈ ∪ 𝑋 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
69	67, 68	sylib 210	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
70	23	funmpt2 6227	. . . . . . . . . . . 12 ⊢ Fun 𝐺
71	23	dmeqi 5623	. . . . . . . . . . . . . . 15 ⊢ dom 𝐺 = dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
72		stoweidlem27.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑄 ∈ V)
73	34	rabexgf 40706	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
75	74	adantr 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
76	75	ex 405	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ 𝑋 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V))
77	22, 76	ralrimi 3166	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
78		dmmptg 5935	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
79	77, 78	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
80	71, 79	syl5eq 2826	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑋)
81	80	eleq2d 2851	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ dom 𝐺 ↔ 𝑤 ∈ 𝑋))
82	81	biimpar 470	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ dom 𝐺)
83		fvelrn 6669	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝑤 ∈ dom 𝐺) → (𝐺‘𝑤) ∈ ran 𝐺)
84	70, 82, 83	sylancr 578	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) ∈ ran 𝐺)
85	84	adantrl 703	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (𝐺‘𝑤) ∈ ran 𝐺)
86	15	ad2antrr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝐹:(1...𝑀)⟶ran 𝐺)
87		simprl 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝑖 ∈ (1...𝑀))
88		fvco3 6588	. . . . . . . . . . . . . 14 ⊢ ((𝐹:(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
89	86, 87, 88	syl2anc 576	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
90		fveq2 6499	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑖) = (𝐺‘𝑤) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
91	90	ad2antll 716	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
92	89, 91	eqtrd 2814	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐺‘𝑤)))
93		eleq1 2853	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
94	93	anbi2d 619	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝜑 ∧ 𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺)))
95		eleq2 2854	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘𝑙) ∈ (𝐺‘𝑤)))
96		fveq2 6499	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑌‘𝑙) = (𝑌‘(𝐺‘𝑤)))
97	96	eleq1d 2850	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ (𝐺‘𝑤) ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
98	95, 97	bitrd 271	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
99	94, 98	imbi12d 337	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (𝐺‘𝑤) → (((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))))
100	99, 29	vtoclg 3486	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
101	100	anabsi7 658	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
102	101	adantr 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
103	92, 102	eqeltrd 2866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
104		f1ofo 6451	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)–onto→ran 𝐺)
105		forn 6422	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺)
106	5, 104, 105	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 = ran 𝐺)
107	106	eleq2d 2851	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
108	107	biimpar 470	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝐺‘𝑤) ∈ ran 𝐹)
109	7	adantr 473	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀))
110		fvelrnb 6556	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn (1...𝑀) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
111	109, 110	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
112	108, 111	mpbid 224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤))
113	103, 112	reximddv 3220	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
114	85, 113	syldan 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
115		simplrl 764	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ 𝑤)
116		simpr 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑋)
117	23	fvmpt2 6605	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ 𝑋 ∧ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
118	116, 75, 117	syl2anc 576	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
119	118	eleq2d 2851	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) ↔ ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
120	119	biimpa 469	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
121	120	adantlrl 707	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
122		nfcv 2932	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ((𝑌 ∘ 𝐹)‘𝑖)
123		nfv 1873	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}
124		fveq1 6498	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (ℎ‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
125	124	breq2d 4941	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (0 < (ℎ‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
126	125	rabbidv 3403	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
127	126	eqeq2d 2788	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
128	122, 34, 123, 127	elrabf 3591	. . . . . . . . . . . . . . . 16 ⊢ (((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
129	121, 128	sylib 210	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
130	129	simprd 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
131	115, 130	eleqtrd 2868	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
132		rabid 3317	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
133	131, 132	sylib 210	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
134	133	simprd 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
135	134	ex 405	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
136	135	reximdv 3218	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
137	114, 136	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
138	137	ex 405	. . . . . . 7 ⊢ (𝜑 → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
139	138	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
140	64, 65, 69, 139	exlimimdd 2149	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
141	140	ex 405	. . . 4 ⊢ (𝜑 → (𝑡 ∈ (𝑇 ∖ 𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
142	62, 141	ralrimi 3166	. . 3 ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
143	13, 61, 142	jca32 508	. 2 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))))
144		feq1 6325	. . . . 5 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄))
145		fveq1 6498	. . . . . . . . 9 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞‘𝑖) = ((𝑌 ∘ 𝐹)‘𝑖))
146	145	fveq1d 6501	. . . . . . . 8 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞‘𝑖)‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
147	146	breq2d 4941	. . . . . . 7 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (0 < ((𝑞‘𝑖)‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
148	147	rexbidv 3242	. . . . . 6 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
149	148	ralbidv 3147	. . . . 5 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
150	144, 149	anbi12d 621	. . . 4 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)) ↔ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))))
151	150	anbi2d 619	. . 3 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))) ↔ (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))))
152	151	spcegv 3516	. 2 ⊢ ((𝑌 ∘ 𝐹) ∈ V → ((𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)))))
153	12, 143, 152	sylc 65	1 ⊢ (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507  ∃wex 1742  Ⅎwnf 1746   ∈ wcel 2050  Ⅎwnfc 2916  ∀wral 3088  ∃wrex 3089  {crab 3092  Vcvv 3415   ∖ cdif 3826   ⊆ wss 3829  ∪ cuni 4712   class class class wbr 4929   ↦ cmpt 5008  dom cdm 5407  ran crn 5408   ∘ ccom 5411  Fun wfun 6182   Fn wfn 6183  ⟶wf 6184  –onto→wfo 6186  –1-1-onto→wf1o 6187  ‘cfv 6188  (class class class)co 6976  0cc0 10335  1c1 10336   < clt 10474  ℕcn 11439  ...cfz 12708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-ov 6979

This theorem is referenced by:  stoweidlem35  41757