Theorem stoweidlem27 42669

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 6957	. . . 4 ⊢ ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V)
4	1, 2, 3	syl2anc 587	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
5		stoweidlem27.7	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
6		f1ofn 6591	. . . . 5 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹 Fn (1...𝑀))
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 Fn (1...𝑀))
8		ovex 7168	. . . 4 ⊢ (1...𝑀) ∈ V
9		fnex 6957	. . . 4 ⊢ ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
10	7, 8, 9	sylancl 589	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
11		coexg 7616	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌 ∘ 𝐹) ∈ V)
12	4, 10, 11	syl2anc 587	. 2 ⊢ (𝜑 → (𝑌 ∘ 𝐹) ∈ V)
13		stoweidlem27.3	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		f1of 6590	. . . . . 6 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)⟶ran 𝐺)
15	5, 14	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶ran 𝐺)
16		fnfco 6517	. . . . 5 ⊢ ((𝑌 Fn ran 𝐺 ∧ 𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌 ∘ 𝐹) Fn (1...𝑀))
17	1, 15, 16	syl2anc 587	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝐹) Fn (1...𝑀))
18		rncoss 5808	. . . . 5 ⊢ ran (𝑌 ∘ 𝐹) ⊆ ran 𝑌
19		fvelrnb 6701	. . . . . . . . . . 11 ⊢ (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
20	1, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
21	20	biimpa 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘)
22		stoweidlem27.10	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤𝜑
23		stoweidlem27.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
24		nfmpt1 5128	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
25	23, 24	nfcxfr 2953	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤𝐺
26	25	nfrn 5788	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑤ran 𝐺
27	26	nfcri 2943	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤 𝑙 ∈ ran 𝐺
28	22, 27	nfan 1900	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑙 ∈ ran 𝐺)
29		stoweidlem27.6	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙)
30	29	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑙)
31		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
32	30, 31	eleqtrd 2892	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
33		nfcv 2955	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ(𝑌‘𝑙)
34		stoweidlem27.11	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ𝑄
35		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}
36		fveq1 6644	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑌‘𝑙) → (ℎ‘𝑡) = ((𝑌‘𝑙)‘𝑡))
37	36	breq2d 5042	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑌‘𝑙) → (0 < (ℎ‘𝑡) ↔ 0 < ((𝑌‘𝑙)‘𝑡)))
38	37	rabbidv 3427	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑌‘𝑙) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)})
39	38	eqeq2d 2809	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑌‘𝑙) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
40	33, 34, 35, 39	elrabf 3624	. . . . . . . . . . . . . . 15 ⊢ ((𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
41	32, 40	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
42	41	simpld 498	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑄)
43		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺)
44	23	elrnmpt 5792	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
45	43, 44	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
46	43, 45	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
47	28, 42, 46	r19.29af 3289	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
48	47	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
49		eleq1 2877	. . . . . . . . . . 11 ⊢ ((𝑌‘𝑙) = 𝑘 → ((𝑌‘𝑙) ∈ 𝑄 ↔ 𝑘 ∈ 𝑄))
50	48, 49	syl5ibcom 248	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌‘𝑙) = 𝑘 → 𝑘 ∈ 𝑄))
51	50	reximdva 3233	. . . . . . . . 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 3242	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄))
56	52, 55	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → 𝑘 ∈ 𝑄)
57	56	ex 416	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 → 𝑘 ∈ 𝑄))
58	57	ssrdv 3921	. . . . 5 ⊢ (𝜑 → ran 𝑌 ⊆ 𝑄)
59	18, 58	sstrid 3926	. . . 4 ⊢ (𝜑 → ran (𝑌 ∘ 𝐹) ⊆ 𝑄)
60		df-f 6328	. . . 4 ⊢ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌 ∘ 𝐹) Fn (1...𝑀) ∧ ran (𝑌 ∘ 𝐹) ⊆ 𝑄))
61	17, 59, 60	sylanbrc 586	. . 3 ⊢ (𝜑 → (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄)
62		stoweidlem27.9	. . . 4 ⊢ Ⅎ𝑡𝜑
63		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑤 𝑡 ∈ (𝑇 ∖ 𝑈)
64	22, 63	nfan 1900	. . . . . 6 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈))
65		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑤∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)
66		stoweidlem27.8	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋)
67	66	sselda 3915	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 𝑡 ∈ ∪ 𝑋)
68		eluni 4803	. . . . . . 7 ⊢ (𝑡 ∈ ∪ 𝑋 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
69	67, 68	sylib 221	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
70	23	funmpt2 6363	. . . . . . . . . . . 12 ⊢ Fun 𝐺
71	23	dmeqi 5737	. . . . . . . . . . . . . . 15 ⊢ dom 𝐺 = dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
72		stoweidlem27.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑄 ∈ V)
73	34	rabexgf 41653	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
75	74	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
76	75	ex 416	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ 𝑋 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V))
77	22, 76	ralrimi 3180	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
78		dmmptg 6063	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
79	77, 78	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
80	71, 79	syl5eq 2845	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑋)
81	80	eleq2d 2875	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ dom 𝐺 ↔ 𝑤 ∈ 𝑋))
82	81	biimpar 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ dom 𝐺)
83		fvelrn 6821	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝑤 ∈ dom 𝐺) → (𝐺‘𝑤) ∈ ran 𝐺)
84	70, 82, 83	sylancr 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) ∈ ran 𝐺)
85	84	adantrl 715	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (𝐺‘𝑤) ∈ ran 𝐺)
86	15	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝐹:(1...𝑀)⟶ran 𝐺)
87		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝑖 ∈ (1...𝑀))
88		fvco3 6737	. . . . . . . . . . . . . 14 ⊢ ((𝐹:(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
89	86, 87, 88	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
90		fveq2 6645	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑖) = (𝐺‘𝑤) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
91	90	ad2antll 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
92	89, 91	eqtrd 2833	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐺‘𝑤)))
93		eleq1 2877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
94	93	anbi2d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝜑 ∧ 𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺)))
95		eleq2 2878	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘𝑙) ∈ (𝐺‘𝑤)))
96		fveq2 6645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑌‘𝑙) = (𝑌‘(𝐺‘𝑤)))
97	96	eleq1d 2874	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ (𝐺‘𝑤) ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
98	95, 97	bitrd 282	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
99	94, 98	imbi12d 348	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (𝐺‘𝑤) → (((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))))
100	99, 29	vtoclg 3515	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
101	100	anabsi7 670	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
102	101	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
103	92, 102	eqeltrd 2890	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
104		f1ofo 6597	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)–onto→ran 𝐺)
105		forn 6568	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺)
106	5, 104, 105	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 = ran 𝐺)
107	106	eleq2d 2875	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
108	107	biimpar 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝐺‘𝑤) ∈ ran 𝐹)
109	7	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀))
110		fvelrnb 6701	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn (1...𝑀) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
111	109, 110	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
112	108, 111	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤))
113	103, 112	reximddv 3234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
114	85, 113	syldan 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
115		simplrl 776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ 𝑤)
116		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑋)
117	23	fvmpt2 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ 𝑋 ∧ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
118	116, 75, 117	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
119	118	eleq2d 2875	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) ↔ ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
120	119	biimpa 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
121	120	adantlrl 719	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
122		nfcv 2955	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ((𝑌 ∘ 𝐹)‘𝑖)
123		nfv 1915	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}
124		fveq1 6644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (ℎ‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
125	124	breq2d 5042	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (0 < (ℎ‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
126	125	rabbidv 3427	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
127	126	eqeq2d 2809	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
128	122, 34, 123, 127	elrabf 3624	. . . . . . . . . . . . . . . 16 ⊢ (((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
129	121, 128	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
130	129	simprd 499	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
131	115, 130	eleqtrd 2892	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
132		rabid 3331	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
133	131, 132	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
134	133	simprd 499	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
135	134	ex 416	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
136	135	reximdv 3232	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
137	114, 136	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
138	137	ex 416	. . . . . . 7 ⊢ (𝜑 → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
139	138	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
140	64, 65, 69, 139	exlimimdd 2217	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
141	140	ex 416	. . . 4 ⊢ (𝜑 → (𝑡 ∈ (𝑇 ∖ 𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
142	62, 141	ralrimi 3180	. . 3 ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
143	13, 61, 142	jca32 519	. 2 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))))
144		feq1 6468	. . . . 5 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄))
145		fveq1 6644	. . . . . . . . 9 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞‘𝑖) = ((𝑌 ∘ 𝐹)‘𝑖))
146	145	fveq1d 6647	. . . . . . . 8 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞‘𝑖)‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
147	146	breq2d 5042	. . . . . . 7 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (0 < ((𝑞‘𝑖)‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
148	147	rexbidv 3256	. . . . . 6 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
149	148	ralbidv 3162	. . . . 5 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
150	144, 149	anbi12d 633	. . . 4 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)) ↔ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))))
151	150	anbi2d 631	. . 3 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))) ↔ (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))))
152	151	spcegv 3545	. 2 ⊢ ((𝑌 ∘ 𝐹) ∈ V → ((𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)))))
153	12, 143, 152	sylc 65	1 ⊢ (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2936  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∖ cdif 3878   ⊆ wss 3881  ∪ cuni 4800   class class class wbr 5030   ↦ cmpt 5110  dom cdm 5519  ran crn 5520   ∘ ccom 5523  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  –onto→wfo 6322  –1-1-onto→wf1o 6323  ‘cfv 6324  (class class class)co 7135  0cc0 10526  1c1 10527   < clt 10664  ℕcn 11625  ...cfz 12885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138

This theorem is referenced by:  stoweidlem35  42677