Theorem cnfcom3lem 9743

Description: Lemma for cnfcom3 9744. (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 ∖ 1o))

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 8202	. . . . . 6 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
4		cnfcom.f	. . . . . . . . 9 ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . 12 ⊢ 𝑆 = dom (ω CNF 𝐴)
6		omelon 9686	. . . . . . . . . . . . 13 ⊢ ω ∈ On
7	6	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ω ∈ On)
8	5, 7, 2	cantnff1o 9736	. . . . . . . . . . 11 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴))
9		f1ocnv 6860	. . . . . . . . . . 11 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆)
10		f1of 6848	. . . . . . . . . . 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 7105	. . . . . . . . 9 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
14	4, 13	eqeltrid 2845	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
15	5, 7, 2	cantnfs 9706	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
16	14, 15	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
17	16	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
18	3, 17	fssdm 6755	. . . . 5 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
19		ovex 7464	. . . . . . . . . . 11 ⊢ (𝐹 supp ∅) ∈ V
20		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
21	20	oion 9576	. . . . . . . . . . 11 ⊢ ((𝐹 supp ∅) ∈ V → dom 𝐺 ∈ On)
22	19, 21	ax-mp 5	. . . . . . . . . 10 ⊢ dom 𝐺 ∈ On
23	22	elexi 3503	. . . . . . . . 9 ⊢ dom 𝐺 ∈ V
24	23	uniex 7761	. . . . . . . 8 ⊢ ∪ dom 𝐺 ∈ V
25	24	sucid 6466	. . . . . . 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 7910	. . . . . . . . . 10 ⊢ ∅ ∈ ω
32	31	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ ω)
33	30, 32	sseldd 3984	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐵)
34	5, 2, 12, 4, 20, 26, 27, 28, 29, 1, 33	cnfcom2lem 9741	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)
35	25, 34	eleqtrrid 2848	. . . . . 6 ⊢ (𝜑 → ∪ dom 𝐺 ∈ dom 𝐺)
36	20	oif 9570	. . . . . . 7 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
37	36	ffvelcdmi 7103	. . . . . 6 ⊢ (∪ dom 𝐺 ∈ dom 𝐺 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
38	35, 37	syl 17	. . . . 5 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
39	18, 38	sseldd 3984	. . . 4 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ 𝐴)
40		onelon 6409	. . . 4 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∪ dom 𝐺) ∈ 𝐴) → (𝐺‘∪ dom 𝐺) ∈ On)
41	2, 39, 40	syl2anc 584	. . 3 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ On)
42	1, 41	eqeltrid 2845	. 2 ⊢ (𝜑 → 𝑊 ∈ On)
43		oecl 8575	. . . . . . 7 ⊢ ((ω ∈ On ∧ 𝐴 ∈ On) → (ω ↑o 𝐴) ∈ On)
44	6, 2, 43	sylancr 587	. . . . . 6 ⊢ (𝜑 → (ω ↑o 𝐴) ∈ On)
45		onelon 6409	. . . . . 6 ⊢ (((ω ↑o 𝐴) ∈ On ∧ 𝐵 ∈ (ω ↑o 𝐴)) → 𝐵 ∈ On)
46	44, 12, 45	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ On)
47		ontri1 6418	. . . . 5 ⊢ ((ω ∈ On ∧ 𝐵 ∈ On) → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
48	6, 46, 47	sylancr 587	. . . 4 ⊢ (𝜑 → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
49	30, 48	mpbid 232	. . 3 ⊢ (𝜑 → ¬ 𝐵 ∈ ω)
50	4	fveq2i 6909	. . . . . . . 8 ⊢ ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵))
51		f1ocnvfv2 7297	. . . . . . . . 9 ⊢ (((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) ∧ 𝐵 ∈ (ω ↑o 𝐴)) → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
52	8, 12, 51	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
53	50, 52	eqtrid 2789	. . . . . . 7 ⊢ (𝜑 → ((ω CNF 𝐴)‘𝐹) = 𝐵)
54	53	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) = 𝐵)
55	6	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ω ∈ On)
56	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐴 ∈ On)
57	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 ∈ 𝑆)
58	31	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ∅ ∈ ω)
59		1on 8518	. . . . . . . . 9 ⊢ 1o ∈ On
60	59	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 1o ∈ On)
61		ovexd 7466	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
62	5, 7, 2, 20, 14	cantnfcl 9707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
63	62	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → E We (𝐹 supp ∅))
64	20	oiiso 9577	. . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
67		isof1o 7343	. . . . . . . . . . . . . . . . . 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 6860	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) → ◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺)
70		f1of 6848	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺 → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
71	68, 69, 70	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
72		ffvelcdm 7101	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝐺:(𝐹 supp ∅)⟶dom 𝐺 ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
73	71, 72	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
74		elssuni 4937	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐺‘𝑥) ∈ dom 𝐺 → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
75	73, 74	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
76		onelon 6409	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐺 ∈ On ∧ (◡𝐺‘𝑥) ∈ dom 𝐺) → (◡𝐺‘𝑥) ∈ On)
77	22, 73, 76	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ On)
78		onuni 7808	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐺 ∈ On → ∪ dom 𝐺 ∈ On)
79	22, 78	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ∪ dom 𝐺 ∈ On
80		ontri1 6418	. . . . . . . . . . . . . . 15 ⊢ (((◡𝐺‘𝑥) ∈ On ∧ ∪ dom 𝐺 ∈ On) → ((◡𝐺‘𝑥) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥)))
81	77, 79, 80	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ((◡𝐺‘𝑥) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥)))
82	75, 81	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥))
83	35	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ∪ dom 𝐺 ∈ dom 𝐺)
84		isorel 7346	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (∪ dom 𝐺 ∈ dom 𝐺 ∧ (◡𝐺‘𝑥) ∈ dom 𝐺)) → (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥))))
85	66, 83, 73, 84	syl12anc 837	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥))))
86		fvex 6919	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐺‘𝑥) ∈ V
87	86	epeli 5586	. . . . . . . . . . . . . . 15 ⊢ (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥))
88	1	breq1i 5150	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(◡𝐺‘𝑥)) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥)))
89		fvex 6919	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘(◡𝐺‘𝑥)) ∈ V
90	89	epeli 5586	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)))
91	88, 90	bitr3i 277	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)))
92	85, 87, 91	3bitr3g 313	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (◡𝐺‘𝑥) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥))))
93		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑊 = ∅)
94		f1ocnvfv2 7297	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
95	68, 94	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
96	93, 95	eleq12d 2835	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)) ↔ ∅ ∈ 𝑥))
97	92, 96	bitrd 279	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (◡𝐺‘𝑥) ↔ ∅ ∈ 𝑥))
98	82, 97	mtbid 324	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∅ ∈ 𝑥)
99		onss 7805	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
100	2, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ⊆ On)
101	18, 100	sstrd 3994	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ On)
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ On)
103	102	sselda 3983	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ On)
104		on0eqel 6508	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
106	105	ord 865	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (¬ 𝑥 = ∅ → ∅ ∈ 𝑥))
107	98, 106	mt3d 148	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 = ∅)
108		el1o 8533	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 1o ↔ 𝑥 = ∅)
109	107, 108	sylibr 234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ 1o)
110	109	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ (𝐹 supp ∅) → 𝑥 ∈ 1o))
111	110	ssrdv 3989	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ 1o)
112	5, 55, 56, 57, 58, 60, 111	cantnflt2 9713	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ (ω ↑o 1o))
113		oe1 8582	. . . . . . . 8 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
114	6, 113	ax-mp 5	. . . . . . 7 ⊢ (ω ↑o 1o) = ω
115	112, 114	eleqtrdi 2851	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ ω)
116	54, 115	eqeltrrd 2842	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐵 ∈ ω)
117	116	ex 412	. . . 4 ⊢ (𝜑 → (𝑊 = ∅ → 𝐵 ∈ ω))
118	117	necon3bd 2954	. . 3 ⊢ (𝜑 → (¬ 𝐵 ∈ ω → 𝑊 ≠ ∅))
119	49, 118	mpd 15	. 2 ⊢ (𝜑 → 𝑊 ≠ ∅)
120		dif1o 8538	. 2 ⊢ (𝑊 ∈ (On ∖ 1o) ↔ (𝑊 ∈ On ∧ 𝑊 ≠ ∅))
121	42, 119, 120	sylanbrc 583	1 ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1o))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480   ∖ cdif 3948   ∪ cun 3949   ⊆ wss 3951  ∅c0 4333  ∪ cuni 4907   class class class wbr 5143   ↦ cmpt 5225   E cep 5583   We wwe 5636  ^◡ccnv 5684  dom cdm 5685  Oncon0 6384  suc csuc 6386  ⟶wf 6557  –1-1-onto→wf1o 6560  ‘cfv 6561   Isom wiso 6562  (class class class)co 7431   ∈ cmpo 7433  ωcom 7887   supp csupp 8185  seq_ωcseqom 8487  1_oc1o 8499   +_o coa 8503   ·_o comu 8504   ↑_o coe 8505   finSupp cfsupp 9401  OrdIsocoi 9549   CNF ccnf 9701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-seqom 8488  df-1o 8506  df-2o 8507  df-oadd 8510  df-omul 8511  df-oexp 8512  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-oi 9550  df-cnf 9702

This theorem is referenced by:  cnfcom3  9744  cnfcom3clem  9745