Metamath Proof Explorer

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 ffvelrnd ⊢ ( 𝜑 → ( ◡ ( ω 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 syl6eqr ⊢ ( ( 𝜑 ∧ 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 syl5eq ⊢ ( 𝜑 → ( ( ω 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 𝐺 )