Theorem cnfcom3lem 8483

Description: Lemma for cnfcom3 8484. (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	⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜 𝐴))
cnfcom.f	⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
cnfcom.g	⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
cnfcom.h	⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅)
cnfcom.t	⊢ 𝑇 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
cnfcom.m	⊢ 𝑀 = ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘)))
cnfcom.k	⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)))
cnfcom.w	⊢ 𝑊 = (𝐺‘∪ dom 𝐺)
cnfcom3.1	⊢ (𝜑 → ω ⊆ 𝐵)

Assertion

Ref	Expression
cnfcom3lem	⊢ (𝜑 → 𝑊 ∈ (On ∖ 1𝑜))

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 7195	. . . . . 6 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
4		cnfcom.f	. . . . . . . . . 10 ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . . 13 ⊢ 𝑆 = dom (ω CNF 𝐴)
6		omelon 8426	. . . . . . . . . . . . . 14 ⊢ ω ∈ On
7	6	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ω ∈ On)
8	5, 7, 2	cantnff1o 8476	. . . . . . . . . . . 12 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴))
9		f1ocnv 6062	. . . . . . . . . . . 12 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴) → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆)
10		f1of 6050	. . . . . . . . . . . 12 ⊢ (◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆)
11	8, 9, 10	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆)
12		cnfcom.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜 𝐴))
13	11, 12	ffvelrnd 6268	. . . . . . . . . 10 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
14	4, 13	syl5eqel 2692	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
15	5, 7, 2	cantnfs 8446	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
16	14, 15	mpbid 221	. . . . . . . 8 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
17	16	simpld 474	. . . . . . 7 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
18		fdm 5964	. . . . . . 7 ⊢ (𝐹:𝐴⟶ω → dom 𝐹 = 𝐴)
19	17, 18	syl 17	. . . . . 6 ⊢ (𝜑 → dom 𝐹 = 𝐴)
20	3, 19	syl5sseq 3616	. . . . 5 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
21		ovex 6577	. . . . . . . . . . 11 ⊢ (𝐹 supp ∅) ∈ V
22		cnfcom.g	. . . . . . . . . . . 12 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
23	22	oion 8324	. . . . . . . . . . 11 ⊢ ((𝐹 supp ∅) ∈ V → dom 𝐺 ∈ On)
24	21, 23	ax-mp 5	. . . . . . . . . 10 ⊢ dom 𝐺 ∈ On
25	24	elexi 3186	. . . . . . . . 9 ⊢ dom 𝐺 ∈ V
26	25	uniex 6851	. . . . . . . 8 ⊢ ∪ dom 𝐺 ∈ V
27	26	sucid 5721	. . . . . . 7 ⊢ ∪ dom 𝐺 ∈ suc ∪ dom 𝐺
28		cnfcom.h	. . . . . . . 8 ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅)
29		cnfcom.t	. . . . . . . 8 ⊢ 𝑇 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
30		cnfcom.m	. . . . . . . 8 ⊢ 𝑀 = ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘)))
31		cnfcom.k	. . . . . . . 8 ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)))
32		cnfcom3.1	. . . . . . . . 9 ⊢ (𝜑 → ω ⊆ 𝐵)
33		peano1 6977	. . . . . . . . . 10 ⊢ ∅ ∈ ω
34	33	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ ω)
35	32, 34	sseldd 3569	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ 𝐵)
36	5, 2, 12, 4, 22, 28, 29, 30, 31, 1, 35	cnfcom2lem 8481	. . . . . . 7 ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)
37	27, 36	syl5eleqr 2695	. . . . . 6 ⊢ (𝜑 → ∪ dom 𝐺 ∈ dom 𝐺)
38	22	oif 8318	. . . . . . 7 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
39	38	ffvelrni 6266	. . . . . 6 ⊢ (∪ dom 𝐺 ∈ dom 𝐺 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
40	37, 39	syl 17	. . . . 5 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ (𝐹 supp ∅))
41	20, 40	sseldd 3569	. . . 4 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ 𝐴)
42		onelon 5665	. . . 4 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∪ dom 𝐺) ∈ 𝐴) → (𝐺‘∪ dom 𝐺) ∈ On)
43	2, 41, 42	syl2anc 691	. . 3 ⊢ (𝜑 → (𝐺‘∪ dom 𝐺) ∈ On)
44	1, 43	syl5eqel 2692	. 2 ⊢ (𝜑 → 𝑊 ∈ On)
45		oecl 7504	. . . . . . 7 ⊢ ((ω ∈ On ∧ 𝐴 ∈ On) → (ω ↑𝑜 𝐴) ∈ On)
46	6, 2, 45	sylancr 694	. . . . . 6 ⊢ (𝜑 → (ω ↑𝑜 𝐴) ∈ On)
47		onelon 5665	. . . . . 6 ⊢ (((ω ↑𝑜 𝐴) ∈ On ∧ 𝐵 ∈ (ω ↑𝑜 𝐴)) → 𝐵 ∈ On)
48	46, 12, 47	syl2anc 691	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ On)
49		ontri1 5674	. . . . 5 ⊢ ((ω ∈ On ∧ 𝐵 ∈ On) → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
50	6, 48, 49	sylancr 694	. . . 4 ⊢ (𝜑 → (ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω))
51	32, 50	mpbid 221	. . 3 ⊢ (𝜑 → ¬ 𝐵 ∈ ω)
52	4	fveq2i 6106	. . . . . . . 8 ⊢ ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵))
53		f1ocnvfv2 6433	. . . . . . . . 9 ⊢ (((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴) ∧ 𝐵 ∈ (ω ↑𝑜 𝐴)) → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
54	8, 12, 53	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
55	52, 54	syl5eq 2656	. . . . . . 7 ⊢ (𝜑 → ((ω CNF 𝐴)‘𝐹) = 𝐵)
56	55	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) = 𝐵)
57	6	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ω ∈ On)
58	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐴 ∈ On)
59	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 ∈ 𝑆)
60	33	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ∅ ∈ ω)
61		1on 7454	. . . . . . . . 9 ⊢ 1𝑜 ∈ On
62	61	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 1𝑜 ∈ On)
63	2, 20	ssexd 4733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
64	5, 7, 2, 22, 14	cantnfcl 8447	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
65	64	simpld 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → E We (𝐹 supp ∅))
66	22	oiiso 8325	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
67	63, 65, 66	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
68	67	ad2antrr 758	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
69		isof1o 6473	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) → 𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅))
70	68, 69	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅))
71		f1ocnv 6062	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) → ◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺)
72		f1of 6050	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺 → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
73	70, 71, 72	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺)
74		ffvelrn 6265	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝐺:(𝐹 supp ∅)⟶dom 𝐺 ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
75	73, 74	sylancom 698	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ dom 𝐺)
76		elssuni 4403	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐺‘𝑥) ∈ dom 𝐺 → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
77	75, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ⊆ ∪ dom 𝐺)
78		onelon 5665	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝐺 ∈ On ∧ (◡𝐺‘𝑥) ∈ dom 𝐺) → (◡𝐺‘𝑥) ∈ On)
79	24, 75, 78	sylancr 694	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (◡𝐺‘𝑥) ∈ On)
80		onuni 6885	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝐺 ∈ On → ∪ dom 𝐺 ∈ On)
81	24, 80	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ∪ dom 𝐺 ∈ On
82		ontri1 5674	. . . . . . . . . . . . . . 15 ⊢ (((◡𝐺‘𝑥) ∈ On ∧ ∪ dom 𝐺 ∈ On) → ((◡𝐺‘𝑥) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥)))
83	79, 81, 82	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ((◡𝐺‘𝑥) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥)))
84	77, 83	mpbid 221	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥))
85	37	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ∪ dom 𝐺 ∈ dom 𝐺)
86		isorel 6476	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (∪ dom 𝐺 ∈ dom 𝐺 ∧ (◡𝐺‘𝑥) ∈ dom 𝐺)) → (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥))))
87	68, 85, 75, 86	syl12anc 1316	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥))))
88		fvex 6113	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐺‘𝑥) ∈ V
89	88	epelc 4951	. . . . . . . . . . . . . . 15 ⊢ (∪ dom 𝐺 E (◡𝐺‘𝑥) ↔ ∪ dom 𝐺 ∈ (◡𝐺‘𝑥))
90	1	breq1i 4590	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(◡𝐺‘𝑥)) ↔ (𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥)))
91		fvex 6113	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘(◡𝐺‘𝑥)) ∈ V
92	91	epelc 4951	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 E (𝐺‘(◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)))
93	90, 92	bitr3i 265	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘∪ dom 𝐺) E (𝐺‘(◡𝐺‘𝑥)) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)))
94	87, 89, 93	3bitr3g 301	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (◡𝐺‘𝑥) ↔ 𝑊 ∈ (𝐺‘(◡𝐺‘𝑥))))
95		simplr 788	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑊 = ∅)
96		f1ocnvfv2 6433	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
97	70, 96	sylancom 698	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝑥)) = 𝑥)
98	95, 97	eleq12d 2682	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑊 ∈ (𝐺‘(◡𝐺‘𝑥)) ↔ ∅ ∈ 𝑥))
99	94, 98	bitrd 267	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (∪ dom 𝐺 ∈ (◡𝐺‘𝑥) ↔ ∅ ∈ 𝑥))
100	84, 99	mtbid 313	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → ¬ ∅ ∈ 𝑥)
101		onss 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
102	2, 101	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ⊆ On)
103	20, 102	sstrd 3578	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ On)
104	103	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ On)
105	104	sselda 3568	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ On)
106		on0eqel 5762	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
107	105, 106	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥))
108	107	ord 391	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → (¬ 𝑥 = ∅ → ∅ ∈ 𝑥))
109	100, 108	mt3d 139	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 = ∅)
110		el1o 7466	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 1𝑜 ↔ 𝑥 = ∅)
111	109, 110	sylibr 223	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ 𝑥 ∈ (𝐹 supp ∅)) → 𝑥 ∈ 1𝑜)
112	111	ex 449	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝑥 ∈ (𝐹 supp ∅) → 𝑥 ∈ 1𝑜))
113	112	ssrdv 3574	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑊 = ∅) → (𝐹 supp ∅) ⊆ 1𝑜)
114	5, 57, 58, 59, 60, 62, 113	cantnflt2 8453	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ (ω ↑𝑜 1𝑜))
115		oe1 7511	. . . . . . . 8 ⊢ (ω ∈ On → (ω ↑𝑜 1𝑜) = ω)
116	6, 115	ax-mp 5	. . . . . . 7 ⊢ (ω ↑𝑜 1𝑜) = ω
117	114, 116	syl6eleq 2698	. . . . . 6 ⊢ ((𝜑 ∧ 𝑊 = ∅) → ((ω CNF 𝐴)‘𝐹) ∈ ω)
118	56, 117	eqeltrrd 2689	. . . . 5 ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐵 ∈ ω)
119	118	ex 449	. . . 4 ⊢ (𝜑 → (𝑊 = ∅ → 𝐵 ∈ ω))
120	119	necon3bd 2796	. . 3 ⊢ (𝜑 → (¬ 𝐵 ∈ ω → 𝑊 ≠ ∅))
121	51, 120	mpd 15	. 2 ⊢ (𝜑 → 𝑊 ≠ ∅)
122		dif1o 7467	. 2 ⊢ (𝑊 ∈ (On ∖ 1𝑜) ↔ (𝑊 ∈ On ∧ 𝑊 ≠ ∅))
123	44, 121, 122	sylanbrc 695	1 ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1𝑜))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  ∪ cuni 4372   class class class wbr 4583   ↦ cmpt 4643   E cep 4947   We wwe 4996  ^◡ccnv 5037  dom cdm 5038  Oncon0 5640  suc csuc 5642  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805  (class class class)co 6549   ↦ cmpt2 6551  ωcom 6957   supp csupp 7182  seq_𝜔cseqom 7429  1_𝑜c1o 7440   +_𝑜 coa 7444   ·_𝑜 comu 7445   ↑_𝑜 coe 7446   finSupp cfsupp 8158  OrdIsocoi 8297   CNF ccnf 8441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-seqom 7430  df-1o 7447  df-2o 7448  df-oadd 7451  df-omul 7452  df-oexp 7453  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-cnf 8442

This theorem is referenced by:  cnfcom3  8484  cnfcom3clem  8485