Theorem stoweidlem27 42319

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 6982	. . . 4 ⊢ ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V)
4	1, 2, 3	syl2anc 586	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
5		stoweidlem27.7	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
6		f1ofn 6618	. . . . 5 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹 Fn (1...𝑀))
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 Fn (1...𝑀))
8		ovex 7191	. . . 4 ⊢ (1...𝑀) ∈ V
9		fnex 6982	. . . 4 ⊢ ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
10	7, 8, 9	sylancl 588	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
11		coexg 7636	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌 ∘ 𝐹) ∈ V)
12	4, 10, 11	syl2anc 586	. 2 ⊢ (𝜑 → (𝑌 ∘ 𝐹) ∈ V)
13		stoweidlem27.3	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		f1of 6617	. . . . . 6 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)⟶ran 𝐺)
15	5, 14	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶ran 𝐺)
16		fnfco 6545	. . . . 5 ⊢ ((𝑌 Fn ran 𝐺 ∧ 𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌 ∘ 𝐹) Fn (1...𝑀))
17	1, 15, 16	syl2anc 586	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝐹) Fn (1...𝑀))
18		rncoss 5845	. . . . 5 ⊢ ran (𝑌 ∘ 𝐹) ⊆ ran 𝑌
19		fvelrnb 6728	. . . . . . . . . . 11 ⊢ (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
20	1, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
21	20	biimpa 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘)
22		stoweidlem27.10	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤𝜑
23		stoweidlem27.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
24		nfmpt1 5166	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
25	23, 24	nfcxfr 2977	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤𝐺
26	25	nfrn 5826	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑤ran 𝐺
27	26	nfcri 2973	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤 𝑙 ∈ ran 𝐺
28	22, 27	nfan 1900	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑙 ∈ ran 𝐺)
29		stoweidlem27.6	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙)
30	29	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑙)
31		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
32	30, 31	eleqtrd 2917	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
33		nfcv 2979	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ(𝑌‘𝑙)
34		stoweidlem27.11	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ𝑄
35		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}
36		fveq1 6671	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑌‘𝑙) → (ℎ‘𝑡) = ((𝑌‘𝑙)‘𝑡))
37	36	breq2d 5080	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑌‘𝑙) → (0 < (ℎ‘𝑡) ↔ 0 < ((𝑌‘𝑙)‘𝑡)))
38	37	rabbidv 3482	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑌‘𝑙) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)})
39	38	eqeq2d 2834	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑌‘𝑙) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
40	33, 34, 35, 39	elrabf 3678	. . . . . . . . . . . . . . 15 ⊢ ((𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
41	32, 40	sylib 220	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
42	41	simpld 497	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑄)
43		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺)
44	23	elrnmpt 5830	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
45	43, 44	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
46	43, 45	mpbid 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
47	28, 42, 46	r19.29af 3333	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
48	47	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
49		eleq1 2902	. . . . . . . . . . 11 ⊢ ((𝑌‘𝑙) = 𝑘 → ((𝑌‘𝑙) ∈ 𝑄 ↔ 𝑘 ∈ 𝑄))
50	48, 49	syl5ibcom 247	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌‘𝑙) = 𝑘 → 𝑘 ∈ 𝑄))
51	50	reximdva 3276	. . . . . . . . 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 3285	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄))
56	52, 55	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → 𝑘 ∈ 𝑄)
57	56	ex 415	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 → 𝑘 ∈ 𝑄))
58	57	ssrdv 3975	. . . . 5 ⊢ (𝜑 → ran 𝑌 ⊆ 𝑄)
59	18, 58	sstrid 3980	. . . 4 ⊢ (𝜑 → ran (𝑌 ∘ 𝐹) ⊆ 𝑄)
60		df-f 6361	. . . 4 ⊢ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌 ∘ 𝐹) Fn (1...𝑀) ∧ ran (𝑌 ∘ 𝐹) ⊆ 𝑄))
61	17, 59, 60	sylanbrc 585	. . 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 3969	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 𝑡 ∈ ∪ 𝑋)
68		eluni 4843	. . . . . . 7 ⊢ (𝑡 ∈ ∪ 𝑋 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
69	67, 68	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
70	23	funmpt2 6396	. . . . . . . . . . . 12 ⊢ Fun 𝐺
71	23	dmeqi 5775	. . . . . . . . . . . . . . 15 ⊢ dom 𝐺 = dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
72		stoweidlem27.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑄 ∈ V)
73	34	rabexgf 41288	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
75	74	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
76	75	ex 415	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ 𝑋 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V))
77	22, 76	ralrimi 3218	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
78		dmmptg 6098	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
79	77, 78	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
80	71, 79	syl5eq 2870	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑋)
81	80	eleq2d 2900	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ dom 𝐺 ↔ 𝑤 ∈ 𝑋))
82	81	biimpar 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ dom 𝐺)
83		fvelrn 6846	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝑤 ∈ dom 𝐺) → (𝐺‘𝑤) ∈ ran 𝐺)
84	70, 82, 83	sylancr 589	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) ∈ ran 𝐺)
85	84	adantrl 714	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (𝐺‘𝑤) ∈ ran 𝐺)
86	15	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝐹:(1...𝑀)⟶ran 𝐺)
87		simprl 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → 𝑖 ∈ (1...𝑀))
88		fvco3 6762	. . . . . . . . . . . . . 14 ⊢ ((𝐹:(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
89	86, 87, 88	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
90		fveq2 6672	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑖) = (𝐺‘𝑤) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
91	90	ad2antll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
92	89, 91	eqtrd 2858	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐺‘𝑤)))
93		eleq1 2902	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
94	93	anbi2d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝜑 ∧ 𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺)))
95		eleq2 2903	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘𝑙) ∈ (𝐺‘𝑤)))
96		fveq2 6672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑌‘𝑙) = (𝑌‘(𝐺‘𝑤)))
97	96	eleq1d 2899	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ (𝐺‘𝑤) ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
98	95, 97	bitrd 281	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
99	94, 98	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (𝐺‘𝑤) → (((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))))
100	99, 29	vtoclg 3569	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
101	100	anabsi7 669	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
102	101	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
103	92, 102	eqeltrd 2915	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
104		f1ofo 6624	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)–onto→ran 𝐺)
105		forn 6595	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺)
106	5, 104, 105	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 = ran 𝐺)
107	106	eleq2d 2900	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
108	107	biimpar 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝐺‘𝑤) ∈ ran 𝐹)
109	7	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀))
110		fvelrnb 6728	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn (1...𝑀) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
111	109, 110	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
112	108, 111	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤))
113	103, 112	reximddv 3277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
114	85, 113	syldan 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
115		simplrl 775	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ 𝑤)
116		simpr 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑋)
117	23	fvmpt2 6781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ 𝑋 ∧ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
118	116, 75, 117	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
119	118	eleq2d 2900	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) ↔ ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
120	119	biimpa 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
121	120	adantlrl 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
122		nfcv 2979	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ((𝑌 ∘ 𝐹)‘𝑖)
123		nfv 1915	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}
124		fveq1 6671	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (ℎ‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
125	124	breq2d 5080	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (0 < (ℎ‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
126	125	rabbidv 3482	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
127	126	eqeq2d 2834	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
128	122, 34, 123, 127	elrabf 3678	. . . . . . . . . . . . . . . 16 ⊢ (((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
129	121, 128	sylib 220	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
130	129	simprd 498	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
131	115, 130	eleqtrd 2917	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
132		rabid 3380	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
133	131, 132	sylib 220	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
134	133	simprd 498	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
135	134	ex 415	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
136	135	reximdv 3275	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
137	114, 136	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
138	137	ex 415	. . . . . . 7 ⊢ (𝜑 → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
139	138	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
140	64, 65, 69, 139	exlimimdd 2219	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
141	140	ex 415	. . . 4 ⊢ (𝜑 → (𝑡 ∈ (𝑇 ∖ 𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
142	62, 141	ralrimi 3218	. . 3 ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
143	13, 61, 142	jca32 518	. 2 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))))
144		feq1 6497	. . . . 5 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄))
145		fveq1 6671	. . . . . . . . 9 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞‘𝑖) = ((𝑌 ∘ 𝐹)‘𝑖))
146	145	fveq1d 6674	. . . . . . . 8 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞‘𝑖)‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
147	146	breq2d 5080	. . . . . . 7 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (0 < ((𝑞‘𝑖)‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
148	147	rexbidv 3299	. . . . . 6 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
149	148	ralbidv 3199	. . . . 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 3599	. 2 ⊢ ((𝑌 ∘ 𝐹) ∈ V → ((𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)))))
153	12, 143, 152	sylc 65	1 ⊢ (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2114  Ⅎwnfc 2963  ∀wral 3140  ∃wrex 3141  {crab 3144  Vcvv 3496   ∖ cdif 3935   ⊆ wss 3938  ∪ cuni 4840   class class class wbr 5068   ↦ cmpt 5148  dom cdm 5557  ran crn 5558   ∘ ccom 5561  Fun wfun 6351   Fn wfn 6352  ⟶wf 6353  –onto→wfo 6355  –1-1-onto→wf1o 6356  ‘cfv 6357  (class class class)co 7158  0cc0 10539  1c1 10540   < clt 10677  ℕcn 11640  ...cfz 12895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161

This theorem is referenced by:  stoweidlem35  42327