Theorem cnfcom3lem 9727

Description: Lemma for cnfcom3 9728. (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 8182	. . . . . 6 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
4		cnfcom.f	. . . . . . . . 9 ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . 12 ⊢ 𝑆 = dom (ω CNF 𝐴)
6		omelon 9670	. . . . . . . . . . . . 13 ⊢ ω ∈ On
7	6	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ω ∈ On)
8	5, 7, 2	cantnff1o 9720	. . . . . . . . . . 11 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴))
9		f1ocnv 6851	. . . . . . . . . . 11 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆)
10		f1of 6839	. . . . . . . . . . 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 7095	. . . . . . . . 9 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
14	4, 13	eqeltrid 2833	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
15	5, 7, 2	cantnfs 9690	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
16	14, 15	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
17	16	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
18	3, 17	fssdm 6742	. . . . 5 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
19		ovex 7453	. . . . . . . . . . 11 ⊢ (𝐹 supp ∅) ∈ V
20		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
21	20	oion 9560	. . . . . . . . . . 11 ⊢ ((𝐹 supp ∅) ∈ V → dom 𝐺 ∈ On)
22	19, 21	ax-mp 5	. . . . . . . . . 10 ⊢ dom 𝐺 ∈ On
23	22	elexi 3491	. . . . . . . . 9 ⊢ dom 𝐺 ∈ V
24	23	uniex 7746	. . . . . . . 8 ⊢ ∪ dom 𝐺 ∈ V
25	24	sucid 6451	. . . . . . 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 7894	. . . . . . . . . 10 ⊢ ∅ ∈ ω
32	31	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ ω)
33	30, 32	sseldd 3981	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐵)
34	5, 2, 12, 4, 20, 26, 27, 28, 29, 1, 33	cnfcom2lem 9725	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)
35	25, 34	eleqtrrid 2836	. . . . . 6 ⊢ (𝜑 → ∪ dom 𝐺 ∈ dom 𝐺)
36	20	oif 9554	. . . . . . 7 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
37	36	ffvelcdmi 7093	. . . . . 6 ⊢ (∪ dom 𝐺 ∈ dom 𝐺 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
38	35, 37	syl 17	. . . . 5 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
39	18, 38	sseldd 3981	. . . 4 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ 𝐴)
40		onelon 6394	. . . 4 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∪ dom 𝐺) ∈ 𝐴) → (𝐺‘∪ dom 𝐺) ∈ On)
41	2, 39, 40	syl2anc 583	. . 3 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ On)
42	1, 41	eqeltrid 2833	. 2 ⊢ (𝜑 → 𝑊 ∈ On)
43		oecl 8558	. . . . . . 7 ⊢ ((ω ∈ On ∧ 𝐴 ∈ On) → (ω ↑o 𝐴) ∈ On)
44	6, 2, 43	sylancr 586	. . . . . 6 ⊢ (𝜑 → (ω ↑o 𝐴) ∈ On)
45		onelon 6394	. . . . . 6 ⊢ (((ω ↑o 𝐴) ∈ On ∧ 𝐵 ∈ (ω ↑o 𝐴)) → 𝐵 ∈ On)
46	44, 12, 45	syl2anc 583	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ On)
47		ontri1 6403	. . . . 5 ⊢ ((ω ∈ On ∧ 𝐵 ∈ On) → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
48	6, 46, 47	sylancr 586	. . . 4 ⊢ (𝜑 → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
49	30, 48	mpbid 231	. . 3 ⊢ (𝜑 → ¬ 𝐵 ∈ ω)
50	4	fveq2i 6900	. . . . . . . 8 ⊢ ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵))
51		f1ocnvfv2 7286	. . . . . . . . 9 ⊢ (((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) ∧ 𝐵 ∈ (ω ↑o 𝐴)) → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
52	8, 12, 51	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
53	50, 52	eqtrid 2780	. . . . . . 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 8499	. . . . . . . . 9 ⊢ 1o ∈ On
60	59	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 1o ∈ On)
61		ovexd 7455	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
62	5, 7, 2, 20, 14	cantnfcl 9691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
63	62	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → E We (𝐹 supp ∅))
64	20	oiiso 9561	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
65	61, 63, 64	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
66	65	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
67		isof1o 7331	. . . . . . . . . . . . . . . . . 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 6851	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) → ◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺)
70		f1of 6839	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺 → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
71	68, 69, 70	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
72		ffvelcdm 7091	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝐺:(𝐹 supp ∅)⟶dom 𝐺 ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
73	71, 72	sylancom 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
74		elssuni 4940	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐺‘𝑥) ∈ dom 𝐺 → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
75	73, 74	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
76		onelon 6394	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐺 ∈ On ∧ (◡𝐺‘𝑥) ∈ dom 𝐺) → (◡𝐺‘𝑥) ∈ On)
77	22, 73, 76	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ On)
78		onuni 7791	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐺 ∈ On → ∪ dom 𝐺 ∈ On)
79	22, 78	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ∪ dom 𝐺 ∈ On
80		ontri1 6403	. . . . . . . . . . . . . . 15 ⊢ (((◡𝐺‘𝑥) ∈ On ∧ ∪ dom 𝐺 ∈ On) → ((◡𝐺‘𝑥) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥)))
81	77, 79, 80	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ((◡𝐺‘𝑥) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥)))
82	75, 81	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥))
83	35	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ∪ dom 𝐺 ∈ dom 𝐺)
84		isorel 7334	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (∪ dom 𝐺 ∈ dom 𝐺 ∧ (◡𝐺‘𝑥) ∈ dom 𝐺)) → (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥))))
85	66, 83, 73, 84	syl12anc 836	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥))))
86		fvex 6910	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐺‘𝑥) ∈ V
87	86	epeli 5584	. . . . . . . . . . . . . . 15 ⊢ (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥))
88	1	breq1i 5155	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(◡𝐺‘𝑥)) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥)))
89		fvex 6910	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘(◡𝐺‘𝑥)) ∈ V
90	89	epeli 5584	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)))
91	88, 90	bitr3i 277	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)))
92	85, 87, 91	3bitr3g 313	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (◡𝐺‘𝑥) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥))))
93		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑊 = ∅)
94		f1ocnvfv2 7286	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
95	68, 94	sylancom 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
96	93, 95	eleq12d 2823	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)) ↔ ∅ ∈ 𝑥))
97	92, 96	bitrd 279	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (◡𝐺‘𝑥) ↔ ∅ ∈ 𝑥))
98	82, 97	mtbid 324	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∅ ∈ 𝑥)
99		onss 7787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
100	2, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ⊆ On)
101	18, 100	sstrd 3990	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ On)
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ On)
103	102	sselda 3980	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ On)
104		on0eqel 6493	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
106	105	ord 863	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (¬ 𝑥 = ∅ → ∅ ∈ 𝑥))
107	98, 106	mt3d 148	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 = ∅)
108		el1o 8516	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 1o ↔ 𝑥 = ∅)
109	107, 108	sylibr 233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ 1o)
110	109	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ (𝐹 supp ∅) → 𝑥 ∈ 1o))
111	110	ssrdv 3986	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ 1o)
112	5, 55, 56, 57, 58, 60, 111	cantnflt2 9697	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ (ω ↑o 1o))
113		oe1 8565	. . . . . . . 8 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
114	6, 113	ax-mp 5	. . . . . . 7 ⊢ (ω ↑o 1o) = ω
115	112, 114	eleqtrdi 2839	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ ω)
116	54, 115	eqeltrrd 2830	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐵 ∈ ω)
117	116	ex 412	. . . 4 ⊢ (𝜑 → (𝑊 = ∅ → 𝐵 ∈ ω))
118	117	necon3bd 2951	. . 3 ⊢ (𝜑 → (¬ 𝐵 ∈ ω → 𝑊 ≠ ∅))
119	49, 118	mpd 15	. 2 ⊢ (𝜑 → 𝑊 ≠ ∅)
120		dif1o 8521	. 2 ⊢ (𝑊 ∈ (On ∖ 1o) ↔ (𝑊 ∈ On ∧ 𝑊 ≠ ∅))
121	42, 119, 120	sylanbrc 582	1 ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1o))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 846   = wceq 1534   ∈ wcel 2099   ≠ wne 2937  Vcvv 3471   ∖ cdif 3944   ∪ cun 3945   ⊆ wss 3947  ∅c0 4323  ∪ cuni 4908   class class class wbr 5148   ↦ cmpt 5231   E cep 5581   We wwe 5632  ^◡ccnv 5677  dom cdm 5678  Oncon0 6369  suc csuc 6371  ⟶wf 6544  –1-1-onto→wf1o 6547  ‘cfv 6548   Isom wiso 6549  (class class class)co 7420   ∈ cmpo 7422  ωcom 7870   supp csupp 8165  seq_ωcseqom 8468  1_oc1o 8480   +_o coa 8484   ·_o comu 8485   ↑_o coe 8486   finSupp cfsupp 9386  OrdIsocoi 9533   CNF ccnf 9685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-inf2 9665

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-isom 6557  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-1st 7993  df-2nd 7994  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-seqom 8469  df-1o 8487  df-2o 8488  df-oadd 8491  df-omul 8492  df-oexp 8493  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9387  df-oi 9534  df-cnf 9686

This theorem is referenced by:  cnfcom3  9728  cnfcom3clem  9729