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 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 𝐺 )