stoweidlem27 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > stoweidlem27		Structured version Visualization version GIF version

Theorem stoweidlem27 44743

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 7219	. . . 4 ⊢ ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V)
4	1, 2, 3	syl2anc 585	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
5		stoweidlem27.7	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
6		f1ofn 6835	. . . . 5 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹 Fn (1...𝑀))
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 Fn (1...𝑀))
8		ovex 7442	. . . 4 ⊢ (1...𝑀) ∈ V
9		fnex 7219	. . . 4 ⊢ ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
10	7, 8, 9	sylancl 587	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
11		coexg 7920	. . 3 ⊢ ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌 ∘ 𝐹) ∈ V)
12	4, 10, 11	syl2anc 585	. 2 ⊢ (𝜑 → (𝑌 ∘ 𝐹) ∈ V)
13		stoweidlem27.3	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14		f1of 6834	. . . . . 6 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)⟶ran 𝐺)
15	5, 14	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶ran 𝐺)
16		fnfco 6757	. . . . 5 ⊢ ((𝑌 Fn ran 𝐺 ∧ 𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌 ∘ 𝐹) Fn (1...𝑀))
17	1, 15, 16	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝐹) Fn (1...𝑀))
18		rncoss 5972	. . . . 5 ⊢ ran (𝑌 ∘ 𝐹) ⊆ ran 𝑌
19		fvelrnb 6953	. . . . . . . . . . 11 ⊢ (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
20	1, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘))
21	20	biimpa 478	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌‘𝑙) = 𝑘)
22		stoweidlem27.10	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤𝜑
23		stoweidlem27.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 = (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
24		nfmpt1 5257	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
25	23, 24	nfcxfr 2902	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑤𝐺
26	25	nfrn 5952	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑤ran 𝐺
27	26	nfcri 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤 𝑙 ∈ ran 𝐺
28	22, 27	nfan 1903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑙 ∈ ran 𝐺)
29		stoweidlem27.6	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙)
30	29	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑙)
31		simpr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
32	30, 31	eleqtrd 2836	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
33		nfcv 2904	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ(𝑌‘𝑙)
34		stoweidlem27.11	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ𝑄
35		nfv 1918	. . . . . . . . . . . . . . . 16 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}
36		fveq1 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑌‘𝑙) → (ℎ‘𝑡) = ((𝑌‘𝑙)‘𝑡))
37	36	breq2d 5161	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑌‘𝑙) → (0 < (ℎ‘𝑡) ↔ 0 < ((𝑌‘𝑙)‘𝑡)))
38	37	rabbidv 3441	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑌‘𝑙) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)})
39	38	eqeq2d 2744	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑌‘𝑙) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
40	33, 34, 35, 39	elrabf 3680	. . . . . . . . . . . . . . 15 ⊢ ((𝑌‘𝑙) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
41	32, 40	sylib 217	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → ((𝑌‘𝑙) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < ((𝑌‘𝑙)‘𝑡)}))
42	41	simpld 496	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑙 ∈ ran 𝐺) ∧ 𝑤 ∈ 𝑋) ∧ 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) → (𝑌‘𝑙) ∈ 𝑄)
43		simpr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺)
44	23	elrnmpt 5956	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
45	43, 44	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
46	43, 45	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → ∃𝑤 ∈ 𝑋 𝑙 = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
47	28, 42, 46	r19.29af 3266	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
48	47	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑄)
49		eleq1 2822	. . . . . . . . . . 11 ⊢ ((𝑌‘𝑙) = 𝑘 → ((𝑌‘𝑙) ∈ 𝑄 ↔ 𝑘 ∈ 𝑄))
50	48, 49	syl5ibcom 244	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌‘𝑙) = 𝑘 → 𝑘 ∈ 𝑄))
51	50	reximdva 3169	. . . . . . . . 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 3154	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄))
56	52, 55	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝑌) → 𝑘 ∈ 𝑄)
57	56	ex 414	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ran 𝑌 → 𝑘 ∈ 𝑄))
58	57	ssrdv 3989	. . . . 5 ⊢ (𝜑 → ran 𝑌 ⊆ 𝑄)
59	18, 58	sstrid 3994	. . . 4 ⊢ (𝜑 → ran (𝑌 ∘ 𝐹) ⊆ 𝑄)
60		df-f 6548	. . . 4 ⊢ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌 ∘ 𝐹) Fn (1...𝑀) ∧ ran (𝑌 ∘ 𝐹) ⊆ 𝑄))
61	17, 59, 60	sylanbrc 584	. . 3 ⊢ (𝜑 → (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄)
62		stoweidlem27.9	. . . 4 ⊢ Ⅎ𝑡𝜑
63		nfv 1918	. . . . . . 7 ⊢ Ⅎ𝑤 𝑡 ∈ (𝑇 ∖ 𝑈)
64	22, 63	nfan 1903	. . . . . 6 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈))
65		nfv 1918	. . . . . 6 ⊢ Ⅎ𝑤∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)
66		stoweidlem27.8	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∖ 𝑈) ⊆ ∪ 𝑋)
67	66	sselda 3983	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 𝑡 ∈ ∪ 𝑋)
68		eluni 4912	. . . . . . 7 ⊢ (𝑡 ∈ ∪ 𝑋 ↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
69	67, 68	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋))
70	23	funmpt2 6588	. . . . . . . . . . . 12 ⊢ Fun 𝐺
71	23	dmeqi 5905	. . . . . . . . . . . . . . 15 ⊢ dom 𝐺 = dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
72		stoweidlem27.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑄 ∈ V)
73	34	rabexgf 43708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ V → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
75	74	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
76	75	ex 414	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ 𝑋 → {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V))
77	22, 76	ralrimi 3255	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V)
78		dmmptg 6242	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝑋 {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
79	77, 78	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑤 ∈ 𝑋 ↦ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}) = 𝑋)
80	71, 79	eqtrid 2785	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑋)
81	80	eleq2d 2820	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ∈ dom 𝐺 ↔ 𝑤 ∈ 𝑋))
82	81	biimpar 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ dom 𝐺)
83		fvelrn 7079	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝑤 ∈ dom 𝐺) → (𝐺‘𝑤) ∈ ran 𝐺)
84	70, 82, 83	sylancr 588	. . . . . . . . . . 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 6991	. . . . . . . . . . . . . 14 ⊢ ((𝐹:(1...𝑀)⟶ran 𝐺 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
89	86, 87, 88	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐹‘𝑖)))
90		fveq2 6892	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑖) = (𝐺‘𝑤) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
91	90	ad2antll 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐹‘𝑖)) = (𝑌‘(𝐺‘𝑤)))
92	89, 91	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) = (𝑌‘(𝐺‘𝑤)))
93		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
94	93	anbi2d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝜑 ∧ 𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺)))
95		eleq2 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘𝑙) ∈ (𝐺‘𝑤)))
96		fveq2 6892	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = (𝐺‘𝑤) → (𝑌‘𝑙) = (𝑌‘(𝐺‘𝑤)))
97	96	eleq1d 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ (𝐺‘𝑤) ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
98	95, 97	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = (𝐺‘𝑤) → ((𝑌‘𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
99	94, 98	imbi12d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = (𝐺‘𝑤) → (((𝜑 ∧ 𝑙 ∈ ran 𝐺) → (𝑌‘𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))))
100	99, 29	vtoclg 3557	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤)))
101	100	anabsi7 670	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
102	101	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → (𝑌‘(𝐺‘𝑤)) ∈ (𝐺‘𝑤))
103	92, 102	eqeltrd 2834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹‘𝑖) = (𝐺‘𝑤))) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
104		f1ofo 6841	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–1-1-onto→ran 𝐺 → 𝐹:(1...𝑀)–onto→ran 𝐺)
105		forn 6809	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺)
106	5, 104, 105	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 = ran 𝐺)
107	106	eleq2d 2820	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ (𝐺‘𝑤) ∈ ran 𝐺))
108	107	biimpar 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → (𝐺‘𝑤) ∈ ran 𝐹)
109	7	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀))
110		fvelrnb 6953	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn (1...𝑀) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
111	109, 110	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ((𝐺‘𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤)))
112	108, 111	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹‘𝑖) = (𝐺‘𝑤))
113	103, 112	reximddv 3172	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐺‘𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
114	85, 113	syldan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤))
115		simplrl 776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ 𝑤)
116		simpr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑋)
117	23	fvmpt2 7010	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ 𝑋 ∧ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ∈ V) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
118	116, 75, 117	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (𝐺‘𝑤) = {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
119	118	eleq2d 2820	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑋) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) ↔ ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}}))
120	119	biimpa 478	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝑋) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
121	120	adantlrl 719	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → ((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}})
122		nfcv 2904	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ((𝑌 ∘ 𝐹)‘𝑖)
123		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎℎ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}
124		fveq1 6891	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (ℎ‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
125	124	breq2d 5161	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (0 < (ℎ‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
126	125	rabbidv 3441	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
127	126	eqeq2d 2744	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = ((𝑌 ∘ 𝐹)‘𝑖) → (𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)} ↔ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
128	122, 34, 123, 127	elrabf 3680	. . . . . . . . . . . . . . . 16 ⊢ (((𝑌 ∘ 𝐹)‘𝑖) ∈ {ℎ ∈ 𝑄 ∣ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (ℎ‘𝑡)}} ↔ (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
129	121, 128	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ 𝑄 ∧ 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)}))
130	129	simprd 497	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑤 = {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
131	115, 130	eleqtrd 2836	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)})
132		rabid 3453	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
133	131, 132	sylib 217	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → (𝑡 ∈ 𝑇 ∧ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
134	133	simprd 497	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) ∧ ((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤)) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
135	134	ex 414	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
136	135	reximdv 3171	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌 ∘ 𝐹)‘𝑖) ∈ (𝐺‘𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
137	114, 136	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
138	137	ex 414	. . . . . . 7 ⊢ (𝜑 → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
139	138	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
140	64, 65, 69, 139	exlimimdd 2213	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
141	140	ex 414	. . . 4 ⊢ (𝜑 → (𝑡 ∈ (𝑇 ∖ 𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
142	62, 141	ralrimi 3255	. . 3 ⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
143	13, 61, 142	jca32 517	. 2 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))))
144		feq1 6699	. . . . 5 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄))
145		fveq1 6891	. . . . . . . . 9 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (𝑞‘𝑖) = ((𝑌 ∘ 𝐹)‘𝑖))
146	145	fveq1d 6894	. . . . . . . 8 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → ((𝑞‘𝑖)‘𝑡) = (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))
147	146	breq2d 5161	. . . . . . 7 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (0 < ((𝑞‘𝑖)‘𝑡) ↔ 0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
148	147	rexbidv 3179	. . . . . 6 ⊢ (𝑞 = (𝑌 ∘ 𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡)))
149	148	ralbidv 3178	. . . . 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 3588	. 2 ⊢ ((𝑌 ∘ 𝐹) ∈ V → ((𝑀 ∈ ℕ ∧ ((𝑌 ∘ 𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌 ∘ 𝐹)‘𝑖)‘𝑡))) → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡)))))
153	12, 143, 152	sylc 65	1 ⊢ (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞‘𝑖)‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∃wex 1782 Ⅎwnf 1786 ∈ wcel 2107 Ⅎwnfc 2884 ∀wral 3062 ∃wrex 3071 {crab 3433 Vcvv 3475 ∖ cdif 3946 ⊆ wss 3949 ∪ cuni 4909 class class class wbr 5149 ↦ cmpt 5232 dom cdm 5677 ran crn 5678 ∘ ccom 5681 Fun wfun 6538 Fn wfn 6539 ⟶wf 6540 –onto→wfo 6542 –1-1-onto→wf1o 6543 ‘cfv 6544 (class class class)co 7409 0cc0 11110 1c1 11111 < clt 11248 ℕcn 12212 ...cfz 13484

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7412

This theorem is referenced by: stoweidlem35 44751

W3C validator