Theorem cnfcom2lem

Description: Lemma for cnfcom2 . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019)

	Ref	Expression
Hypotheses	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 𝐺 )
	cnfcom2.1	⊢ ( 𝜑 → ∅ ∈ 𝐵 )
Assertion	cnfcom2lem	⊢ ( 𝜑 → dom 𝐺 = suc ∪ dom 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		cnfcom.s	⊢ 𝑆 = dom ( ω CNF 𝐴 )
2		cnfcom.a	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cnfcom.b	⊢ ( 𝜑 → 𝐵 ∈ ( ω ↑o 𝐴 ) )
4		cnfcom.f	⊢ 𝐹 = ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 )
5		cnfcom.g	⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
6		cnfcom.h	⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ )
7		cnfcom.t	⊢ 𝑇 = seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) , ∅ )
8		cnfcom.m	⊢ 𝑀 = ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
9		cnfcom.k	⊢ 𝐾 = ( ( 𝑥 ∈ 𝑀 ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑥 ) ) )
10		cnfcom.w	⊢ 𝑊 = ( 𝐺 ‘ ∪ dom 𝐺 )
11		cnfcom2.1	⊢ ( 𝜑 → ∅ ∈ 𝐵 )
12		n0i	⊢ ( ∅ ∈ 𝐵 → ¬ 𝐵 = ∅ )
13	11 12	syl	⊢ ( 𝜑 → ¬ 𝐵 = ∅ )
14		omelon	⊢ ω ∈ On
15	14	a1i	⊢ ( 𝜑 → ω ∈ On )
16	1 15 2	cantnff1o	⊢ ( 𝜑 → ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) )
17		f1ocnv	⊢ ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 )
18		f1of	⊢ ( ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
19	16 17 18	3syl	⊢ ( 𝜑 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
20	19 3	ffvelcdmd	⊢ ( 𝜑 → ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ∈ 𝑆 )
21	4 20	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
22	1 15 2	cantnfs	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
23	21 22	mpbid	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) )
24	23	simpld	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ω )
25	24	adantr	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → 𝐹 : 𝐴 ⟶ ω )
26	25	feqmptd	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
27		dif0	⊢ ( 𝐴 ∖ ∅ ) = 𝐴
28	27	eleq2i	⊢ ( 𝑥 ∈ ( 𝐴 ∖ ∅ ) ↔ 𝑥 ∈ 𝐴 )
29		simpr	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → dom 𝐺 = ∅ )
30		ovexd	⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ V )
31	1 15 2 5 21	cantnfcl	⊢ ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom 𝐺 ∈ ω ) )
32	31	simpld	⊢ ( 𝜑 → E We ( 𝐹 supp ∅ ) )
33	5	oien	⊢ ( ( ( 𝐹 supp ∅ ) ∈ V ∧ E We ( 𝐹 supp ∅ ) ) → dom 𝐺 ≈ ( 𝐹 supp ∅ ) )
34	30 32 33	syl2anc	⊢ ( 𝜑 → dom 𝐺 ≈ ( 𝐹 supp ∅ ) )
35	34	adantr	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → dom 𝐺 ≈ ( 𝐹 supp ∅ ) )
36	29 35	eqbrtrrd	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → ∅ ≈ ( 𝐹 supp ∅ ) )
37	36	ensymd	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → ( 𝐹 supp ∅ ) ≈ ∅ )
38		en0	⊢ ( ( 𝐹 supp ∅ ) ≈ ∅ ↔ ( 𝐹 supp ∅ ) = ∅ )
39	37 38	sylib	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → ( 𝐹 supp ∅ ) = ∅ )
40		ss0b	⊢ ( ( 𝐹 supp ∅ ) ⊆ ∅ ↔ ( 𝐹 supp ∅ ) = ∅ )
41	39 40	sylibr	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → ( 𝐹 supp ∅ ) ⊆ ∅ )
42	2	adantr	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → 𝐴 ∈ On )
43		0ex	⊢ ∅ ∈ V
44	43	a1i	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → ∅ ∈ V )
45	25 41 42 44	suppssr	⊢ ( ( ( 𝜑 ∧ dom 𝐺 = ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∖ ∅ ) ) → ( 𝐹 ‘ 𝑥 ) = ∅ )
46	28 45	sylan2br	⊢ ( ( ( 𝜑 ∧ dom 𝐺 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ∅ )
47	46	mpteq2dva	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ∅ ) )
48	26 47	eqtrd	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ∅ ) )
49		fconstmpt	⊢ ( 𝐴 × { ∅ } ) = ( 𝑥 ∈ 𝐴 ↦ ∅ )
50	48 49	eqtr4di	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → 𝐹 = ( 𝐴 × { ∅ } ) )
51	50	fveq2d	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = ( ( ω CNF 𝐴 ) ‘ ( 𝐴 × { ∅ } ) ) )
52	4	fveq2i	⊢ ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) )
53		f1ocnvfv2	⊢ ( ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) ∧ 𝐵 ∈ ( ω ↑o 𝐴 ) ) → ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) = 𝐵 )
54	16 3 53	syl2anc	⊢ ( 𝜑 → ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) = 𝐵 )
55	52 54	eqtrid	⊢ ( 𝜑 → ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = 𝐵 )
56	55	adantr	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = 𝐵 )
57		peano1	⊢ ∅ ∈ ω
58	57	a1i	⊢ ( 𝜑 → ∅ ∈ ω )
59	1 15 2 58	cantnf0	⊢ ( 𝜑 → ( ( ω CNF 𝐴 ) ‘ ( 𝐴 × { ∅ } ) ) = ∅ )
60	59	adantr	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → ( ( ω CNF 𝐴 ) ‘ ( 𝐴 × { ∅ } ) ) = ∅ )
61	51 56 60	3eqtr3d	⊢ ( ( 𝜑 ∧ dom 𝐺 = ∅ ) → 𝐵 = ∅ )
62	13 61	mtand	⊢ ( 𝜑 → ¬ dom 𝐺 = ∅ )
63		nnlim	⊢ ( dom 𝐺 ∈ ω → ¬ Lim dom 𝐺 )
64	31 63	simpl2im	⊢ ( 𝜑 → ¬ Lim dom 𝐺 )
65		ioran	⊢ ( ¬ ( dom 𝐺 = ∅ ∨ Lim dom 𝐺 ) ↔ ( ¬ dom 𝐺 = ∅ ∧ ¬ Lim dom 𝐺 ) )
66	62 64 65	sylanbrc	⊢ ( 𝜑 → ¬ ( dom 𝐺 = ∅ ∨ Lim dom 𝐺 ) )
67	5	oicl	⊢ Ord dom 𝐺
68		unizlim	⊢ ( Ord dom 𝐺 → ( dom 𝐺 = ∪ dom 𝐺 ↔ ( dom 𝐺 = ∅ ∨ Lim dom 𝐺 ) ) )
69	67 68	ax-mp	⊢ ( dom 𝐺 = ∪ dom 𝐺 ↔ ( dom 𝐺 = ∅ ∨ Lim dom 𝐺 ) )
70	66 69	sylnibr	⊢ ( 𝜑 → ¬ dom 𝐺 = ∪ dom 𝐺 )
71		orduniorsuc	⊢ ( Ord dom 𝐺 → ( dom 𝐺 = ∪ dom 𝐺 ∨ dom 𝐺 = suc ∪ dom 𝐺 ) )
72	67 71	mp1i	⊢ ( 𝜑 → ( dom 𝐺 = ∪ dom 𝐺 ∨ dom 𝐺 = suc ∪ dom 𝐺 ) )
73	72	ord	⊢ ( 𝜑 → ( ¬ dom 𝐺 = ∪ dom 𝐺 → dom 𝐺 = suc ∪ dom 𝐺 ) )
74	70 73	mpd	⊢ ( 𝜑 → dom 𝐺 = suc ∪ dom 𝐺 )