Metamath Proof Explorer

Theorem cnfcom3lem

Description: Lemma for cnfcom3 . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 4-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 𝐺 )
cnfcom3.1 ⊢ ( 𝜑 → ω ⊆ 𝐵 )
Assertion cnfcom3lem ( 𝜑 → 𝑊 ∈ ( On ∖ 1o ) )

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 cnfcom3.1 ⊢ ( 𝜑 → ω ⊆ 𝐵 )
12 suppssdm ⊢ ( 𝐹 supp ∅ ) ⊆ dom 𝐹
13 omelon ⊢ ω ∈ On
14 13 a1i ⊢ ( 𝜑 → ω ∈ On )
15 1 14 2 cantnff1o ⊢ ( 𝜑 → ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) )
16 f1ocnv ⊢ ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 )
17 f1of ⊢ ( ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
18 15 16 17 3syl ⊢ ( 𝜑 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
19 18 3 ffvelrnd ⊢ ( 𝜑 → ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ∈ 𝑆 )
20 4 19 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
21 1 14 2 cantnfs ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
22 20 21 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) )
23 22 simpld ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ω )
24 12 23 fssdm ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ 𝐴 )
25 ovex ⊢ ( 𝐹 supp ∅ ) ∈ V
26 5 oion ⊢ ( ( 𝐹 supp ∅ ) ∈ V → dom 𝐺 ∈ On )
27 25 26 ax-mp ⊢ dom 𝐺 ∈ On
28 27 elexi ⊢ dom 𝐺 ∈ V
29 28 uniex ⊢ ∪ dom 𝐺 ∈ V
30 29 sucid ⊢ ∪ dom 𝐺 ∈ suc ∪ dom 𝐺
31 peano1 ⊢ ∅ ∈ ω
32 31 a1i ⊢ ( 𝜑 → ∅ ∈ ω )
33 11 32 sseldd ⊢ ( 𝜑 → ∅ ∈ 𝐵 )
34 1 2 3 4 5 6 7 8 9 10 33 cnfcom2lem ⊢ ( 𝜑 → dom 𝐺 = suc ∪ dom 𝐺 )
35 30 34 eleqtrrid ⊢ ( 𝜑 → ∪ dom 𝐺 ∈ dom 𝐺 )
36 5 oif ⊢ 𝐺 : dom 𝐺 ⟶ ( 𝐹 supp ∅ )
37 36 ffvelrni ⊢ ( ∪ dom 𝐺 ∈ dom 𝐺 → ( 𝐺 ‘ ∪ dom 𝐺 ) ∈ ( 𝐹 supp ∅ ) )
38 35 37 syl ⊢ ( 𝜑 → ( 𝐺 ‘ ∪ dom 𝐺 ) ∈ ( 𝐹 supp ∅ ) )
39 24 38 sseldd ⊢ ( 𝜑 → ( 𝐺 ‘ ∪ dom 𝐺 ) ∈ 𝐴 )
40 onelon ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐺 ‘ ∪ dom 𝐺 ) ∈ 𝐴 ) → ( 𝐺 ‘ ∪ dom 𝐺 ) ∈ On )
41 2 39 40 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ ∪ dom 𝐺 ) ∈ On )
42 10 41 eqeltrid ⊢ ( 𝜑 → 𝑊 ∈ On )
43 oecl ⊢ ( ( ω ∈ On ∧ 𝐴 ∈ On ) → ( ω ↑o 𝐴 ) ∈ On )
44 13 2 43 sylancr ⊢ ( 𝜑 → ( ω ↑o 𝐴 ) ∈ On )
45 onelon ⊢ ( ( ( ω ↑o 𝐴 ) ∈ On ∧ 𝐵 ∈ ( ω ↑o 𝐴 ) ) → 𝐵 ∈ On )
46 44 3 45 syl2anc ⊢ ( 𝜑 → 𝐵 ∈ On )
47 ontri1 ⊢ ( ( ω ∈ On ∧ 𝐵 ∈ On ) → ( ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω ) )
48 13 46 47 sylancr ⊢ ( 𝜑 → ( ω ⊆ 𝐵 ↔ ¬ 𝐵 ∈ ω ) )
49 11 48 mpbid ⊢ ( 𝜑 → ¬ 𝐵 ∈ ω )
50 4 fveq2i ⊢ ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) )
51 f1ocnvfv2 ⊢ ( ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) ∧ 𝐵 ∈ ( ω ↑o 𝐴 ) ) → ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) = 𝐵 )
52 15 3 51 syl2anc ⊢ ( 𝜑 → ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) = 𝐵 )
53 50 52 eqtrid ⊢ ( 𝜑 → ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = 𝐵 )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = 𝐵 )
55 13 a1i ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ω ∈ On )
56 2 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐴 ∈ On )
57 20 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐹 ∈ 𝑆 )
58 31 a1i ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ∅ ∈ ω )
59 1on ⊢ 1o ∈ On
60 59 a1i ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 1o ∈ On )
61 ovexd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ V )
62 1 14 2 5 20 cantnfcl ⊢ ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom 𝐺 ∈ ω ) )
63 62 simpld ⊢ ( 𝜑 → E We ( 𝐹 supp ∅ ) )
64 5 oiiso ⊢ ( ( ( 𝐹 supp ∅ ) ∈ V ∧ E We ( 𝐹 supp ∅ ) ) → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
65 61 63 64 syl2anc ⊢ ( 𝜑 → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
66 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) )
67 isof1o ⊢ ( 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) → 𝐺 : dom 𝐺 –1-1-onto→ ( 𝐹 supp ∅ ) )
68 66 67 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → 𝐺 : dom 𝐺 –1-1-onto→ ( 𝐹 supp ∅ ) )
69 f1ocnv ⊢ ( 𝐺 : dom 𝐺 –1-1-onto→ ( 𝐹 supp ∅ ) → ◡ 𝐺 : ( 𝐹 supp ∅ ) –1-1-onto→ dom 𝐺 )
70 f1of ⊢ ( ◡ 𝐺 : ( 𝐹 supp ∅ ) –1-1-onto→ dom 𝐺 → ◡ 𝐺 : ( 𝐹 supp ∅ ) ⟶ dom 𝐺 )
71 68 69 70 3syl ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ◡ 𝐺 : ( 𝐹 supp ∅ ) ⟶ dom 𝐺 )
72 ffvelrn ⊢ ( ( ◡ 𝐺 : ( 𝐹 supp ∅ ) ⟶ dom 𝐺 ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( ◡ 𝐺 ‘ 𝑥 ) ∈ dom 𝐺 )
73 71 72 sylancom ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( ◡ 𝐺 ‘ 𝑥 ) ∈ dom 𝐺 )
74 elssuni ⊢ ( ( ◡ 𝐺 ‘ 𝑥 ) ∈ dom 𝐺 → ( ◡ 𝐺 ‘ 𝑥 ) ⊆ ∪ dom 𝐺 )
75 73 74 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( ◡ 𝐺 ‘ 𝑥 ) ⊆ ∪ dom 𝐺 )
76 onelon ⊢ ( ( dom 𝐺 ∈ On ∧ ( ◡ 𝐺 ‘ 𝑥 ) ∈ dom 𝐺 ) → ( ◡ 𝐺 ‘ 𝑥 ) ∈ On )
77 27 73 76 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( ◡ 𝐺 ‘ 𝑥 ) ∈ On )
78 onuni ⊢ ( dom 𝐺 ∈ On → ∪ dom 𝐺 ∈ On )
79 27 78 ax-mp ⊢ ∪ dom 𝐺 ∈ On
80 ontri1 ⊢ ( ( ( ◡ 𝐺 ‘ 𝑥 ) ∈ On ∧ ∪ dom 𝐺 ∈ On ) → ( ( ◡ 𝐺 ‘ 𝑥 ) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ ( ◡ 𝐺 ‘ 𝑥 ) ) )
81 77 79 80 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( ( ◡ 𝐺 ‘ 𝑥 ) ⊆ ∪ dom 𝐺 ↔ ¬ ∪ dom 𝐺 ∈ ( ◡ 𝐺 ‘ 𝑥 ) ) )
82 75 81 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ¬ ∪ dom 𝐺 ∈ ( ◡ 𝐺 ‘ 𝑥 ) )
83 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ∪ dom 𝐺 ∈ dom 𝐺 )
84 isorel ⊢ ( ( 𝐺 Isom E , E ( dom 𝐺 , ( 𝐹 supp ∅ ) ) ∧ ( ∪ dom 𝐺 ∈ dom 𝐺 ∧ ( ◡ 𝐺 ‘ 𝑥 ) ∈ dom 𝐺 ) ) → ( ∪ dom 𝐺 E ( ◡ 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ ∪ dom 𝐺 ) E ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) ) )
85 66 83 73 84 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( ∪ dom 𝐺 E ( ◡ 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ ∪ dom 𝐺 ) E ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) ) )
86 fvex ⊢ ( ◡ 𝐺 ‘ 𝑥 ) ∈ V
87 86 epeli ⊢ ( ∪ dom 𝐺 E ( ◡ 𝐺 ‘ 𝑥 ) ↔ ∪ dom 𝐺 ∈ ( ◡ 𝐺 ‘ 𝑥 ) )
88 10 breq1i ⊢ ( 𝑊 E ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐺 ‘ ∪ dom 𝐺 ) E ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) )
89 fvex ⊢ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) ∈ V
90 89 epeli ⊢ ( 𝑊 E ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) ↔ 𝑊 ∈ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) )
91 88 90 bitr3i ⊢ ( ( 𝐺 ‘ ∪ dom 𝐺 ) E ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) ↔ 𝑊 ∈ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) )
92 85 87 91 3bitr3g ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( ∪ dom 𝐺 ∈ ( ◡ 𝐺 ‘ 𝑥 ) ↔ 𝑊 ∈ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) ) )
93 simplr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → 𝑊 = ∅ )
94 f1ocnvfv2 ⊢ ( ( 𝐺 : dom 𝐺 –1-1-onto→ ( 𝐹 supp ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) = 𝑥 )
95 68 94 sylancom ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) = 𝑥 )
96 93 95 eleq12d ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( 𝑊 ∈ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑥 ) ) ↔ ∅ ∈ 𝑥 ) )
97 92 96 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( ∪ dom 𝐺 ∈ ( ◡ 𝐺 ‘ 𝑥 ) ↔ ∅ ∈ 𝑥 ) )
98 82 97 mtbid ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ¬ ∅ ∈ 𝑥 )
99 onss ⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
100 2 99 syl ⊢ ( 𝜑 → 𝐴 ⊆ On )
101 24 100 sstrd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ On )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐹 supp ∅ ) ⊆ On )
103 102 sselda ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → 𝑥 ∈ On )
104 on0eqel ⊢ ( 𝑥 ∈ On → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
105 103 104 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
106 105 ord ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → ( ¬ 𝑥 = ∅ → ∅ ∈ 𝑥 ) )
107 98 106 mt3d ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → 𝑥 = ∅ )
108 el1o ⊢ ( 𝑥 ∈ 1o ↔ 𝑥 = ∅ )
109 107 108 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ ( 𝐹 supp ∅ ) ) → 𝑥 ∈ 1o )
110 109 ex ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝑥 ∈ ( 𝐹 supp ∅ ) → 𝑥 ∈ 1o ) )
111 110 ssrdv ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐹 supp ∅ ) ⊆ 1o )
112 1 55 56 57 58 60 111 cantnflt2 ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( ( ω CNF 𝐴 ) ‘ 𝐹 ) ∈ ( ω ↑o 1o ) )
113 oe1 ⊢ ( ω ∈ On → ( ω ↑o 1o ) = ω )
114 13 113 ax-mp ⊢ ( ω ↑o 1o ) = ω
115 112 114 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( ( ω CNF 𝐴 ) ‘ 𝐹 ) ∈ ω )
116 54 115 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐵 ∈ ω )
117 116 ex ⊢ ( 𝜑 → ( 𝑊 = ∅ → 𝐵 ∈ ω ) )
118 117 necon3bd ⊢ ( 𝜑 → ( ¬ 𝐵 ∈ ω → 𝑊 ≠ ∅ ) )
119 49 118 mpd ⊢ ( 𝜑 → 𝑊 ≠ ∅ )
120 dif1o ⊢ ( 𝑊 ∈ ( On ∖ 1o ) ↔ ( 𝑊 ∈ On ∧ 𝑊 ≠ ∅ ) )
121 42 119 120 sylanbrc ⊢ ( 𝜑 → 𝑊 ∈ ( On ∖ 1o ) )