Theorem cnfcom3lem 9391

Description: Lemma for cnfcom3 9392. (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 7964	. . . . . 6 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
4		cnfcom.f	. . . . . . . . 9 ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . 12 ⊢ 𝑆 = dom (ω CNF 𝐴)
6		omelon 9334	. . . . . . . . . . . . 13 ⊢ ω ∈ On
7	6	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ω ∈ On)
8	5, 7, 2	cantnff1o 9384	. . . . . . . . . . 11 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴))
9		f1ocnv 6712	. . . . . . . . . . 11 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆)
10		f1of 6700	. . . . . . . . . . 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	ffvelrnd 6944	. . . . . . . . 9 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
14	4, 13	eqeltrid 2843	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
15	5, 7, 2	cantnfs 9354	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
16	14, 15	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
17	16	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
18	3, 17	fssdm 6604	. . . . 5 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
19		ovex 7288	. . . . . . . . . . 11 ⊢ (𝐹 supp ∅) ∈ V
20		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
21	20	oion 9225	. . . . . . . . . . 11 ⊢ ((𝐹 supp ∅) ∈ V → dom 𝐺 ∈ On)
22	19, 21	ax-mp 5	. . . . . . . . . 10 ⊢ dom 𝐺 ∈ On
23	22	elexi 3441	. . . . . . . . 9 ⊢ dom 𝐺 ∈ V
24	23	uniex 7572	. . . . . . . 8 ⊢ ∪ dom 𝐺 ∈ V
25	24	sucid 6330	. . . . . . 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 7710	. . . . . . . . . 10 ⊢ ∅ ∈ ω
32	31	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ ω)
33	30, 32	sseldd 3918	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐵)
34	5, 2, 12, 4, 20, 26, 27, 28, 29, 1, 33	cnfcom2lem 9389	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)
35	25, 34	eleqtrrid 2846	. . . . . 6 ⊢ (𝜑 → ∪ dom 𝐺 ∈ dom 𝐺)
36	20	oif 9219	. . . . . . 7 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
37	36	ffvelrni 6942	. . . . . 6 ⊢ (∪ dom 𝐺 ∈ dom 𝐺 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
38	35, 37	syl 17	. . . . 5 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
39	18, 38	sseldd 3918	. . . 4 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ 𝐴)
40		onelon 6276	. . . 4 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∪ dom 𝐺) ∈ 𝐴) → (𝐺‘∪ dom 𝐺) ∈ On)
41	2, 39, 40	syl2anc 583	. . 3 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ On)
42	1, 41	eqeltrid 2843	. 2 ⊢ (𝜑 → 𝑊 ∈ On)
43		oecl 8329	. . . . . . 7 ⊢ ((ω ∈ On ∧ 𝐴 ∈ On) → (ω ↑o 𝐴) ∈ On)
44	6, 2, 43	sylancr 586	. . . . . 6 ⊢ (𝜑 → (ω ↑o 𝐴) ∈ On)
45		onelon 6276	. . . . . 6 ⊢ (((ω ↑o 𝐴) ∈ On ∧ 𝐵 ∈ (ω ↑o 𝐴)) → 𝐵 ∈ On)
46	44, 12, 45	syl2anc 583	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ On)
47		ontri1 6285	. . . . 5 ⊢ ((ω ∈ On ∧ 𝐵 ∈ On) → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
48	6, 46, 47	sylancr 586	. . . 4 ⊢ (𝜑 → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
49	30, 48	mpbid 231	. . 3 ⊢ (𝜑 → ¬ 𝐵 ∈ ω)
50	4	fveq2i 6759	. . . . . . . 8 ⊢ ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵))
51		f1ocnvfv2 7130	. . . . . . . . 9 ⊢ (((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) ∧ 𝐵 ∈ (ω ↑o 𝐴)) → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
52	8, 12, 51	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
53	50, 52	eqtrid 2790	. . . . . . 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 8274	. . . . . . . . 9 ⊢ 1o ∈ On
60	59	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 1o ∈ On)
61		ovexd 7290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
62	5, 7, 2, 20, 14	cantnfcl 9355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
63	62	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → E We (𝐹 supp ∅))
64	20	oiiso 9226	. . . . . . . . . . . . . . . . . . . 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 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
67		isof1o 7174	. . . . . . . . . . . . . . . . . 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 6712	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) → ◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺)
70		f1of 6700	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺 → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
71	68, 69, 70	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
72		ffvelrn 6941	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝐺:(𝐹 supp ∅)⟶dom 𝐺 ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
73	71, 72	sylancom 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
74		elssuni 4868	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐺‘𝑥) ∈ dom 𝐺 → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
75	73, 74	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
76		onelon 6276	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐺 ∈ On ∧ (◡𝐺‘𝑥) ∈ dom 𝐺) → (◡𝐺‘𝑥) ∈ On)
77	22, 73, 76	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ On)
78		onuni 7615	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐺 ∈ On → ∪ dom 𝐺 ∈ On)
79	22, 78	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ∪ dom 𝐺 ∈ On
80		ontri1 6285	. . . . . . . . . . . . . . 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 722	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ∪ dom 𝐺 ∈ dom 𝐺)
84		isorel 7177	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (∪ dom 𝐺 ∈ dom 𝐺 ∧ (◡𝐺‘𝑥) ∈ dom 𝐺)) → (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥))))
85	66, 83, 73, 84	syl12anc 833	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥))))
86		fvex 6769	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐺‘𝑥) ∈ V
87	86	epeli 5488	. . . . . . . . . . . . . . 15 ⊢ (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥))
88	1	breq1i 5077	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(◡𝐺‘𝑥)) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥)))
89		fvex 6769	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘(◡𝐺‘𝑥)) ∈ V
90	89	epeli 5488	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)))
91	88, 90	bitr3i 276	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)))
92	85, 87, 91	3bitr3g 312	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (◡𝐺‘𝑥) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥))))
93		simplr 765	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑊 = ∅)
94		f1ocnvfv2 7130	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
95	68, 94	sylancom 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
96	93, 95	eleq12d 2833	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)) ↔ ∅ ∈ 𝑥))
97	92, 96	bitrd 278	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (◡𝐺‘𝑥) ↔ ∅ ∈ 𝑥))
98	82, 97	mtbid 323	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∅ ∈ 𝑥)
99		onss 7611	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
100	2, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ⊆ On)
101	18, 100	sstrd 3927	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ On)
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ On)
103	102	sselda 3917	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ On)
104		on0eqel 6369	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
106	105	ord 860	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (¬ 𝑥 = ∅ → ∅ ∈ 𝑥))
107	98, 106	mt3d 148	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 = ∅)
108		el1o 8291	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 1o ↔ 𝑥 = ∅)
109	107, 108	sylibr 233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ 1o)
110	109	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ (𝐹 supp ∅) → 𝑥 ∈ 1o))
111	110	ssrdv 3923	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ 1o)
112	5, 55, 56, 57, 58, 60, 111	cantnflt2 9361	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ (ω ↑o 1o))
113		oe1 8337	. . . . . . . 8 ⊢ (ω ∈ On → (ω ↑o 1o) = ω)
114	6, 113	ax-mp 5	. . . . . . 7 ⊢ (ω ↑o 1o) = ω
115	112, 114	eleqtrdi 2849	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ ω)
116	54, 115	eqeltrrd 2840	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐵 ∈ ω)
117	116	ex 412	. . . 4 ⊢ (𝜑 → (𝑊 = ∅ → 𝐵 ∈ ω))
118	117	necon3bd 2956	. . 3 ⊢ (𝜑 → (¬ 𝐵 ∈ ω → 𝑊 ≠ ∅))
119	49, 118	mpd 15	. 2 ⊢ (𝜑 → 𝑊 ≠ ∅)
120		dif1o 8292	. 2 ⊢ (𝑊 ∈ (On ∖ 1o) ↔ (𝑊 ∈ On ∧ 𝑊 ≠ ∅))
121	42, 119, 120	sylanbrc 582	1 ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1o))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  ∅c0 4253  ∪ cuni 4836   class class class wbr 5070   ↦ cmpt 5153   E cep 5485   We wwe 5534  ^◡ccnv 5579  dom cdm 5580  Oncon0 6251  suc csuc 6253  ⟶wf 6414  –1-1-onto→wf1o 6417  ‘cfv 6418   Isom wiso 6419  (class class class)co 7255   ∈ cmpo 7257  ωcom 7687   supp csupp 7948  seq_ωcseqom 8248  1_oc1o 8260   +_o coa 8264   ·_o comu 8265   ↑_o coe 8266   finSupp cfsupp 9058  OrdIsocoi 9198   CNF ccnf 9349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-supp 7949  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-seqom 8249  df-1o 8267  df-2o 8268  df-oadd 8271  df-omul 8272  df-oexp 8273  df-er 8456  df-map 8575  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-fsupp 9059  df-oi 9199  df-cnf 9350

This theorem is referenced by:  cnfcom3  9392  cnfcom3clem  9393