cnfcom3lem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cnfcom3lem		Structured version Visualization version GIF version

Theorem cnfcom3lem 9694

Description: Lemma for cnfcom3 9695. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 4-Jul-2019.)

**Hypotheses**
Ref	Expression
cnfcom.s	⊢ 𝑆 = dom (ω CNF 𝐴)
cnfcom.a	⊢ (𝜑 → 𝐴 ∈ On)
cnfcom.b	⊢ (𝜑 → 𝐵 ∈ (ω ↑_o 𝐴))
cnfcom.f	⊢ 𝐹 = (^◡(ω CNF 𝐴)‘𝐵)
cnfcom.g	⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
cnfcom.h	⊢ 𝐻 = seq_ω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +_o 𝑧)), ∅)
cnfcom.t	⊢ 𝑇 = seq_ω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
cnfcom.m	⊢ 𝑀 = ((ω ↑_o (𝐺‘𝑘)) ·_o (𝐹‘(𝐺‘𝑘)))
cnfcom.k	⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +_o 𝑥)) ∪ ^◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +_o 𝑥)))
cnfcom.w	⊢ 𝑊 = (𝐺‘∪ dom 𝐺)
cnfcom3.1	⊢ (𝜑 → ω ⊆ 𝐵)

**Assertion**
Ref	Expression
cnfcom3lem	⊢ (𝜑 → 𝑊 ∈ (On ∖ 1_o))

Distinct variable groups: 𝑥,𝑘,𝑧,𝐴 𝑥,𝑀 𝑓,𝑘,𝑥,𝑧,𝐹 𝑧,𝑇 𝑥,𝑊 𝑓,𝐺,𝑘,𝑥,𝑧 𝑓,𝐻,𝑥 𝑆,𝑘,𝑧 𝜑,𝑘,𝑥,𝑧 Allowed substitution hints: 𝜑(𝑓) 𝐴(𝑓) 𝐵(𝑥,𝑧,𝑓,𝑘) 𝑆(𝑥,𝑓) 𝑇(𝑥,𝑓,𝑘) 𝐻(𝑧,𝑘) 𝐾(𝑥,𝑧,𝑓,𝑘) 𝑀(𝑧,𝑓,𝑘) 𝑊(𝑧,𝑓,𝑘)

**Proof of Theorem cnfcom3lem**
Step	Hyp	Ref	Expression
1		cnfcom.w	. . 3 ⊢ 𝑊 = (𝐺‘∪ dom 𝐺)
2		cnfcom.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ On)
3		suppssdm 8158	. . . . . 6 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
4		cnfcom.f	. . . . . . . . 9 ⊢ 𝐹 = (^◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . 12 ⊢ 𝑆 = dom (ω CNF 𝐴)
6		omelon 9637	. . . . . . . . . . . . 13 ⊢ ω ∈ On
7	6	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ω ∈ On)
8	5, 7, 2	cantnff1o 9687	. . . . . . . . . . 11 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑_o 𝐴))
9		f1ocnv 6842	. . . . . . . . . . 11 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑_o 𝐴) → ^◡(ω CNF 𝐴):(ω ↑_o 𝐴)–1-1-onto→𝑆)
10		f1of 6830	. . . . . . . . . . 11 ⊢ (^◡(ω CNF 𝐴):(ω ↑_o 𝐴)–1-1-onto→𝑆 → ^◡(ω CNF 𝐴):(ω ↑_o 𝐴)⟶𝑆)
11	8, 9, 10	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ^◡(ω CNF 𝐴):(ω ↑_o 𝐴)⟶𝑆)
12		cnfcom.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ (ω ↑_o 𝐴))
13	11, 12	ffvelcdmd 7084	. . . . . . . . 9 ⊢ (𝜑 → (^◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
14	4, 13	eqeltrid 2837	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
15	5, 7, 2	cantnfs 9657	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
16	14, 15	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
17	16	simpld 495	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
18	3, 17	fssdm 6734	. . . . 5 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
19		ovex 7438	. . . . . . . . . . 11 ⊢ (𝐹 supp ∅) ∈ V
20		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
21	20	oion 9527	. . . . . . . . . . 11 ⊢ ((𝐹 supp ∅) ∈ V → dom 𝐺 ∈ On)
22	19, 21	ax-mp 5	. . . . . . . . . 10 ⊢ dom 𝐺 ∈ On
23	22	elexi 3493	. . . . . . . . 9 ⊢ dom 𝐺 ∈ V
24	23	uniex 7727	. . . . . . . 8 ⊢ ∪ dom 𝐺 ∈ V
25	24	sucid 6443	. . . . . . 7 ⊢ ∪ dom 𝐺 ∈ suc ∪ dom 𝐺
26		cnfcom.h	. . . . . . . 8 ⊢ 𝐻 = seq_ω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +_o 𝑧)), ∅)
27		cnfcom.t	. . . . . . . 8 ⊢ 𝑇 = seq_ω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
28		cnfcom.m	. . . . . . . 8 ⊢ 𝑀 = ((ω ↑_o (𝐺‘𝑘)) ·_o (𝐹‘(𝐺‘𝑘)))
29		cnfcom.k	. . . . . . . 8 ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +_o 𝑥)) ∪ ^◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +_o 𝑥)))
30		cnfcom3.1	. . . . . . . . 9 ⊢ (𝜑 → ω ⊆ 𝐵)
31		peano1 7875	. . . . . . . . . 10 ⊢ ∅ ∈ ω
32	31	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ ω)
33	30, 32	sseldd 3982	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐵)
34	5, 2, 12, 4, 20, 26, 27, 28, 29, 1, 33	cnfcom2lem 9692	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)
35	25, 34	eleqtrrid 2840	. . . . . 6 ⊢ (𝜑 → ∪ dom 𝐺 ∈ dom 𝐺)
36	20	oif 9521	. . . . . . 7 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
37	36	ffvelcdmi 7082	. . . . . 6 ⊢ (∪ dom 𝐺 ∈ dom 𝐺 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
38	35, 37	syl 17	. . . . 5 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
39	18, 38	sseldd 3982	. . . 4 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ 𝐴)
40		onelon 6386	. . . 4 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∪ dom 𝐺) ∈ 𝐴) → (𝐺‘∪ dom 𝐺) ∈ On)
41	2, 39, 40	syl2anc 584	. . 3 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ On)
42	1, 41	eqeltrid 2837	. 2 ⊢ (𝜑 → 𝑊 ∈ On)
43		oecl 8533	. . . . . . 7 ⊢ ((ω ∈ On ∧ 𝐴 ∈ On) → (ω ↑_o 𝐴) ∈ On)
44	6, 2, 43	sylancr 587	. . . . . 6 ⊢ (𝜑 → (ω ↑_o 𝐴) ∈ On)
45		onelon 6386	. . . . . 6 ⊢ (((ω ↑_o 𝐴) ∈ On ∧ 𝐵 ∈ (ω ↑_o 𝐴)) → 𝐵 ∈ On)
46	44, 12, 45	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ On)
47		ontri1 6395	. . . . 5 ⊢ ((ω ∈ On ∧ 𝐵 ∈ On) → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
48	6, 46, 47	sylancr 587	. . . 4 ⊢ (𝜑 → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
49	30, 48	mpbid 231	. . 3 ⊢ (𝜑 → ¬ 𝐵 ∈ ω)
50	4	fveq2i 6891	. . . . . . . 8 ⊢ ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(^◡(ω CNF 𝐴)‘𝐵))
51		f1ocnvfv2 7271	. . . . . . . . 9 ⊢ (((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑_o 𝐴) ∧ 𝐵 ∈ (ω ↑_o 𝐴)) → ((ω CNF 𝐴)‘(^◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
52	8, 12, 51	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((ω CNF 𝐴)‘(^◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
53	50, 52	eqtrid 2784	. . . . . . 7 ⊢ (𝜑 → ((ω CNF 𝐴)‘𝐹) = 𝐵)
54	53	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) = 𝐵)
55	6	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ω ∈ On)
56	2	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐴 ∈ On)
57	14	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 ∈ 𝑆)
58	31	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ∅ ∈ ω)
59		1on 8474	. . . . . . . . 9 ⊢ 1_o ∈ On
60	59	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 1_o ∈ On)
61		ovexd 7440	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
62	5, 7, 2, 20, 14	cantnfcl 9658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
63	62	simpld 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → E We (𝐹 supp ∅))
64	20	oiiso 9528	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
65	61, 63, 64	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
66	65	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
67		isof1o 7316	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) → 𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅))
68	66, 67	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅))
69		f1ocnv 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) → ^◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺)
70		f1of 6830	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺 → ^◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
71	68, 69, 70	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ^◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
72		ffvelcdm 7080	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐺:(𝐹 supp ∅)⟶dom 𝐺 ∧ 𝑥 ∈ (𝐹 supp ∅)) → (^◡𝐺‘𝑥) ∈ dom 𝐺)
73	71, 72	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (^◡𝐺‘𝑥) ∈ dom 𝐺)
74		elssuni 4940	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐺‘𝑥) ∈ dom 𝐺 → (^◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
75	73, 74	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (^◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
76		onelon 6386	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐺 ∈ On ∧ (^◡𝐺‘𝑥) ∈ dom 𝐺) → (^◡𝐺‘𝑥) ∈ On)
77	22, 73, 76	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (^◡𝐺‘𝑥) ∈ On)
78		onuni 7772	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐺 ∈ On → ∪ dom 𝐺 ∈ On)
79	22, 78	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ∪ dom 𝐺 ∈ On
80		ontri1 6395	. . . . . . . . . . . . . . 15 ⊢ (((^◡𝐺‘𝑥) ∈ On ∧ ∪ dom 𝐺 ∈ On) → ((^◡𝐺‘𝑥) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ (^◡𝐺‘𝑥)))
81	77, 79, 80	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ((^◡𝐺‘𝑥) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ (^◡𝐺‘𝑥)))
82	75, 81	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∪ dom 𝐺 ∈ (^◡𝐺‘𝑥))
83	35	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ∪ dom 𝐺 ∈ dom 𝐺)
84		isorel 7319	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (∪ dom 𝐺 ∈ dom 𝐺 ∧ (^◡𝐺‘𝑥) ∈ dom 𝐺)) → (∪ dom 𝐺 E (^◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(^◡𝐺‘𝑥))))
85	66, 83, 73, 84	syl12anc 835	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 E (^◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(^◡𝐺‘𝑥))))
86		fvex 6901	. . . . . . . . . . . . . . . 16 ⊢ (^◡𝐺‘𝑥) ∈ V
87	86	epeli 5581	. . . . . . . . . . . . . . 15 ⊢ (∪ dom 𝐺 E (^◡𝐺‘𝑥) ↔ ∪ dom 𝐺 ∈ (^◡𝐺‘𝑥))
88	1	breq1i 5154	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(^◡𝐺‘𝑥)) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(^◡𝐺‘𝑥)))
89		fvex 6901	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘(^◡𝐺‘𝑥)) ∈ V
90	89	epeli 5581	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(^◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(^◡𝐺‘𝑥)))
91	88, 90	bitr3i 276	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘∪ dom 𝐺) E (𝐺‘(^◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(^◡𝐺‘𝑥)))
92	85, 87, 91	3bitr3g 312	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (^◡𝐺‘𝑥) ↔ 𝑊 ∈ (𝐺‘(^◡𝐺‘𝑥))))
93		simplr 767	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑊 = ∅)
94		f1ocnvfv2 7271	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(^◡𝐺‘𝑥)) = 𝑥)
95	68, 94	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(^◡𝐺‘𝑥)) = 𝑥)
96	93, 95	eleq12d 2827	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑊 ∈ (𝐺‘(^◡𝐺‘𝑥)) ↔ ∅ ∈ 𝑥))
97	92, 96	bitrd 278	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (^◡𝐺‘𝑥) ↔ ∅ ∈ 𝑥))
98	82, 97	mtbid 323	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∅ ∈ 𝑥)
99		onss 7768	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
100	2, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ⊆ On)
101	18, 100	sstrd 3991	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ On)
102	101	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ On)
103	102	sselda 3981	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ On)
104		on0eqel 6485	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
106	105	ord 862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (¬ 𝑥 = ∅ → ∅ ∈ 𝑥))
107	98, 106	mt3d 148	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 = ∅)
108		el1o 8491	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 1_o ↔ 𝑥 = ∅)
109	107, 108	sylibr 233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ 1_o)
110	109	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ (𝐹 supp ∅) → 𝑥 ∈ 1_o))
111	110	ssrdv 3987	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ 1_o)
112	5, 55, 56, 57, 58, 60, 111	cantnflt2 9664	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ (ω ↑_o 1_o))
113		oe1 8540	. . . . . . . 8 ⊢ (ω ∈ On → (ω ↑_o 1_o) = ω)
114	6, 113	ax-mp 5	. . . . . . 7 ⊢ (ω ↑_o 1_o) = ω
115	112, 114	eleqtrdi 2843	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ ω)
116	54, 115	eqeltrrd 2834	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐵 ∈ ω)
117	116	ex 413	. . . 4 ⊢ (𝜑 → (𝑊 = ∅ → 𝐵 ∈ ω))
118	117	necon3bd 2954	. . 3 ⊢ (𝜑 → (¬ 𝐵 ∈ ω → 𝑊 ≠ ∅))
119	49, 118	mpd 15	. 2 ⊢ (𝜑 → 𝑊 ≠ ∅)
120		dif1o 8496	. 2 ⊢ (𝑊 ∈ (On ∖ 1_o) ↔ (𝑊 ∈ On ∧ 𝑊 ≠ ∅))
121	42, 119, 120	sylanbrc 583	1 ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1_o))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 Vcvv 3474 ∖ cdif 3944 ∪ cun 3945 ⊆ wss 3947 ∅c0 4321 ∪ cuni 4907 class class class wbr 5147 ↦ cmpt 5230 E cep 5578 We wwe 5629 ^◡ccnv 5674 dom cdm 5675 Oncon0 6361 suc csuc 6363 ⟶wf 6536 –1-1-onto→wf1o 6539 ‘cfv 6540 Isom wiso 6541 (class class class)co 7405 ∈ cmpo 7407 ωcom 7851 supp csupp 8142 seq_ωcseqom 8443 1_oc1o 8455 +_o coa 8459 ·_o comu 8460 ↑_o coe 8461 finSupp cfsupp 9357 OrdIsocoi 9500 CNF ccnf 9652

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-inf2 9632

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-supp 8143 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-seqom 8444 df-1o 8462 df-2o 8463 df-oadd 8466 df-omul 8467 df-oexp 8468 df-er 8699 df-map 8818 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-fsupp 9358 df-oi 9501 df-cnf 9653

This theorem is referenced by: cnfcom3 9695 cnfcom3clem 9696

W3C validator