Theorem cnfcom3lem 9618

Description: Lemma for cnfcom3 9619. (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 8117	. . . . . 6 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
4		cnfcom.f	. . . . . . . . 9 ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . 12 ⊢ 𝑆 = dom (ω CNF 𝐴)
6		omelon 9561	. . . . . . . . . . . . 13 ⊢ ω ∈ On
7	6	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ω ∈ On)
8	5, 7, 2	cantnff1o 9611	. . . . . . . . . . 11 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴))
9		f1ocnv 6780	. . . . . . . . . . 11 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆)
10		f1of 6768	. . . . . . . . . . 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 7023	. . . . . . . . 9 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
14	4, 13	eqeltrid 2832	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
15	5, 7, 2	cantnfs 9581	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
16	14, 15	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
17	16	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
18	3, 17	fssdm 6675	. . . . 5 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
19		ovex 7386	. . . . . . . . . . 11 ⊢ (𝐹 supp ∅) ∈ V
20		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
21	20	oion 9447	. . . . . . . . . . 11 ⊢ ((𝐹 supp ∅) ∈ V → dom 𝐺 ∈ On)
22	19, 21	ax-mp 5	. . . . . . . . . 10 ⊢ dom 𝐺 ∈ On
23	22	elexi 3461	. . . . . . . . 9 ⊢ dom 𝐺 ∈ V
24	23	uniex 7681	. . . . . . . 8 ⊢ ∪ dom 𝐺 ∈ V
25	24	sucid 6395	. . . . . . 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 7829	. . . . . . . . . 10 ⊢ ∅ ∈ ω
32	31	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ ω)
33	30, 32	sseldd 3938	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐵)
34	5, 2, 12, 4, 20, 26, 27, 28, 29, 1, 33	cnfcom2lem 9616	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)
35	25, 34	eleqtrrid 2835	. . . . . 6 ⊢ (𝜑 → ∪ dom 𝐺 ∈ dom 𝐺)
36	20	oif 9441	. . . . . . 7 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
37	36	ffvelcdmi 7021	. . . . . 6 ⊢ (∪ dom 𝐺 ∈ dom 𝐺 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
38	35, 37	syl 17	. . . . 5 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
39	18, 38	sseldd 3938	. . . 4 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ 𝐴)
40		onelon 6336	. . . 4 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∪ dom 𝐺) ∈ 𝐴) → (𝐺‘∪ dom 𝐺) ∈ On)
41	2, 39, 40	syl2anc 584	. . 3 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ On)
42	1, 41	eqeltrid 2832	. 2 ⊢ (𝜑 → 𝑊 ∈ On)
43		oecl 8462	. . . . . . 7 ⊢ ((ω ∈ On ∧ 𝐴 ∈ On) → (ω ↑o 𝐴) ∈ On)
44	6, 2, 43	sylancr 587	. . . . . 6 ⊢ (𝜑 → (ω ↑o 𝐴) ∈ On)
45		onelon 6336	. . . . . 6 ⊢ (((ω ↑o 𝐴) ∈ On ∧ 𝐵 ∈ (ω ↑o 𝐴)) → 𝐵 ∈ On)
46	44, 12, 45	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ On)
47		ontri1 6345	. . . . 5 ⊢ ((ω ∈ On ∧ 𝐵 ∈ On) → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
48	6, 46, 47	sylancr 587	. . . 4 ⊢ (𝜑 → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
49	30, 48	mpbid 232	. . 3 ⊢ (𝜑 → ¬ 𝐵 ∈ ω)
50	4	fveq2i 6829	. . . . . . . 8 ⊢ ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵))
51		f1ocnvfv2 7218	. . . . . . . . 9 ⊢ (((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) ∧ 𝐵 ∈ (ω ↑o 𝐴)) → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
52	8, 12, 51	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
53	50, 52	eqtrid 2776	. . . . . . 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 8407	. . . . . . . . 9 ⊢ 1o ∈ On
60	59	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 1o ∈ On)
61		ovexd 7388	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
62	5, 7, 2, 20, 14	cantnfcl 9582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
63	62	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → E We (𝐹 supp ∅))
64	20	oiiso 9448	. . . . . . . . . . . . . . . . . . . 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 7264	. . . . . . . . . . . . . . . . . 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 6780	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) → ◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺)
70		f1of 6768	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺 → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
71	68, 69, 70	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
72		ffvelcdm 7019	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝐺:(𝐹 supp ∅)⟶dom 𝐺 ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
73	71, 72	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
74		elssuni 4891	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐺‘𝑥) ∈ dom 𝐺 → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
75	73, 74	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
76		onelon 6336	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐺 ∈ On ∧ (◡𝐺‘𝑥) ∈ dom 𝐺) → (◡𝐺‘𝑥) ∈ On)
77	22, 73, 76	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ On)
78		onuni 7728	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐺 ∈ On → ∪ dom 𝐺 ∈ On)
79	22, 78	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ∪ dom 𝐺 ∈ On
80		ontri1 6345	. . . . . . . . . . . . . . 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 7267	. . . . . . . . . . . . . . . 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 6839	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐺‘𝑥) ∈ V
87	86	epeli 5525	. . . . . . . . . . . . . . 15 ⊢ (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥))
88	1	breq1i 5102	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(◡𝐺‘𝑥)) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥)))
89		fvex 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘(◡𝐺‘𝑥)) ∈ V
90	89	epeli 5525	. . . . . . . . . . . . . . . 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 7218	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
95	68, 94	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
96	93, 95	eleq12d 2822	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)) ↔ ∅ ∈ 𝑥))
97	92, 96	bitrd 279	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (◡𝐺‘𝑥) ↔ ∅ ∈ 𝑥))
98	82, 97	mtbid 324	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∅ ∈ 𝑥)
99		onss 7725	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
100	2, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ⊆ On)
101	18, 100	sstrd 3948	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ On)
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ On)
103	102	sselda 3937	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ On)
104		on0eqel 6436	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
106	105	ord 864	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (¬ 𝑥 = ∅ → ∅ ∈ 𝑥))
107	98, 106	mt3d 148	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 = ∅)
108		el1o 8420	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 1o ↔ 𝑥 = ∅)
109	107, 108	sylibr 234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ 1o)
110	109	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ (𝐹 supp ∅) → 𝑥 ∈ 1o))
111	110	ssrdv 3943	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ 1o)
112	5, 55, 56, 57, 58, 60, 111	cantnflt2 9588	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ (ω ↑o 1o))
113		oe1 8469	. . . . . . . 8 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
114	6, 113	ax-mp 5	. . . . . . 7 ⊢ (ω ↑o 1o) = ω
115	112, 114	eleqtrdi 2838	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ ω)
116	54, 115	eqeltrrd 2829	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐵 ∈ ω)
117	116	ex 412	. . . 4 ⊢ (𝜑 → (𝑊 = ∅ → 𝐵 ∈ ω))
118	117	necon3bd 2939	. . 3 ⊢ (𝜑 → (¬ 𝐵 ∈ ω → 𝑊 ≠ ∅))
119	49, 118	mpd 15	. 2 ⊢ (𝜑 → 𝑊 ≠ ∅)
120		dif1o 8425	. 2 ⊢ (𝑊 ∈ (On ∖ 1o) ↔ (𝑊 ∈ On ∧ 𝑊 ≠ ∅))
121	42, 119, 120	sylanbrc 583	1 ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1o))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  Vcvv 3438   ∖ cdif 3902   ∪ cun 3903   ⊆ wss 3905  ∅c0 4286  ∪ cuni 4861   class class class wbr 5095   ↦ cmpt 5176   E cep 5522   We wwe 5575  ^◡ccnv 5622  dom cdm 5623  Oncon0 6311  suc csuc 6313  ⟶wf 6482  –1-1-onto→wf1o 6485  ‘cfv 6486   Isom wiso 6487  (class class class)co 7353   ∈ cmpo 7355  ωcom 7806   supp csupp 8100  seq_ωcseqom 8376  1_oc1o 8388   +_o coa 8392   ·_o comu 8393   ↑_o coe 8394   finSupp cfsupp 9270  OrdIsocoi 9420   CNF ccnf 9576

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-inf2 9556

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-int 4900  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-se 5577  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-seqom 8377  df-1o 8395  df-2o 8396  df-oadd 8399  df-omul 8400  df-oexp 8401  df-er 8632  df-map 8762  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9271  df-oi 9421  df-cnf 9577

This theorem is referenced by:  cnfcom3  9619  cnfcom3clem  9620