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 
|- S = dom ( _om CNF A )
cnfcom.a 
|- ( ph -> A e. On )
cnfcom.b 
|- ( ph -> B e. ( _om ^o A ) )
cnfcom.f 
|- F = ( `' ( _om CNF A ) ` B )
cnfcom.g 
|- G = OrdIso ( _E , ( F supp (/) ) )
cnfcom.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )
cnfcom.t 
|- T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) )
cnfcom.m 
|- M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )
cnfcom.k 
|- K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )
cnfcom.w 
|- W = ( G ` U. dom G )
cnfcom3.1 
|- ( ph -> _om C_ B )
Assertion cnfcom3lem 
|- ( ph -> W e. ( On \ 1o ) )

Proof

Step Hyp Ref Expression
1 cnfcom.s 
 |-  S = dom ( _om CNF A )
2 cnfcom.a 
 |-  ( ph -> A e. On )
3 cnfcom.b 
 |-  ( ph -> B e. ( _om ^o A ) )
4 cnfcom.f 
 |-  F = ( `' ( _om CNF A ) ` B )
5 cnfcom.g 
 |-  G = OrdIso ( _E , ( F supp (/) ) )
6 cnfcom.h 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )
7 cnfcom.t 
 |-  T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) )
8 cnfcom.m 
 |-  M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )
9 cnfcom.k 
 |-  K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )
10 cnfcom.w 
 |-  W = ( G ` U. dom G )
11 cnfcom3.1 
 |-  ( ph -> _om C_ B )
12 suppssdm 
 |-  ( F supp (/) ) C_ dom F
13 omelon 
 |-  _om e. On
14 13 a1i 
 |-  ( ph -> _om e. On )
15 1 14 2 cantnff1o 
 |-  ( ph -> ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) )
16 f1ocnv 
 |-  ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) -> `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S )
17 f1of 
 |-  ( `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
18 15 16 17 3syl 
 |-  ( ph -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
19 18 3 ffvelcdmd 
 |-  ( ph -> ( `' ( _om CNF A ) ` B ) e. S )
20 4 19 eqeltrid 
 |-  ( ph -> F e. S )
21 1 14 2 cantnfs 
 |-  ( ph -> ( F e. S <-> ( F : A --> _om /\ F finSupp (/) ) ) )
22 20 21 mpbid 
 |-  ( ph -> ( F : A --> _om /\ F finSupp (/) ) )
23 22 simpld 
 |-  ( ph -> F : A --> _om )
24 12 23 fssdm 
 |-  ( ph -> ( F supp (/) ) C_ A )
25 ovex 
 |-  ( F supp (/) ) e. _V
26 5 oion 
 |-  ( ( F supp (/) ) e. _V -> dom G e. On )
27 25 26 ax-mp 
 |-  dom G e. On
28 27 elexi 
 |-  dom G e. _V
29 28 uniex 
 |-  U. dom G e. _V
30 29 sucid 
 |-  U. dom G e. suc U. dom G
31 peano1 
 |-  (/) e. _om
32 31 a1i 
 |-  ( ph -> (/) e. _om )
33 11 32 sseldd 
 |-  ( ph -> (/) e. B )
34 1 2 3 4 5 6 7 8 9 10 33 cnfcom2lem 
 |-  ( ph -> dom G = suc U. dom G )
35 30 34 eleqtrrid 
 |-  ( ph -> U. dom G e. dom G )
36 5 oif 
 |-  G : dom G --> ( F supp (/) )
37 36 ffvelcdmi 
 |-  ( U. dom G e. dom G -> ( G ` U. dom G ) e. ( F supp (/) ) )
38 35 37 syl 
 |-  ( ph -> ( G ` U. dom G ) e. ( F supp (/) ) )
39 24 38 sseldd 
 |-  ( ph -> ( G ` U. dom G ) e. A )
40 onelon 
 |-  ( ( A e. On /\ ( G ` U. dom G ) e. A ) -> ( G ` U. dom G ) e. On )
41 2 39 40 syl2anc 
 |-  ( ph -> ( G ` U. dom G ) e. On )
42 10 41 eqeltrid 
 |-  ( ph -> W e. On )
43 oecl 
 |-  ( ( _om e. On /\ A e. On ) -> ( _om ^o A ) e. On )
44 13 2 43 sylancr 
 |-  ( ph -> ( _om ^o A ) e. On )
45 onelon 
 |-  ( ( ( _om ^o A ) e. On /\ B e. ( _om ^o A ) ) -> B e. On )
46 44 3 45 syl2anc 
 |-  ( ph -> B e. On )
47 ontri1 
 |-  ( ( _om e. On /\ B e. On ) -> ( _om C_ B <-> -. B e. _om ) )
48 13 46 47 sylancr 
 |-  ( ph -> ( _om C_ B <-> -. B e. _om ) )
49 11 48 mpbid 
 |-  ( ph -> -. B e. _om )
50 4 fveq2i 
 |-  ( ( _om CNF A ) ` F ) = ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) )
51 f1ocnvfv2 
 |-  ( ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) /\ B e. ( _om ^o A ) ) -> ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) = B )
52 15 3 51 syl2anc 
 |-  ( ph -> ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) = B )
53 50 52 eqtrid 
 |-  ( ph -> ( ( _om CNF A ) ` F ) = B )
54 53 adantr 
 |-  ( ( ph /\ W = (/) ) -> ( ( _om CNF A ) ` F ) = B )
55 13 a1i 
 |-  ( ( ph /\ W = (/) ) -> _om e. On )
56 2 adantr 
 |-  ( ( ph /\ W = (/) ) -> A e. On )
57 20 adantr 
 |-  ( ( ph /\ W = (/) ) -> F e. S )
58 31 a1i 
 |-  ( ( ph /\ W = (/) ) -> (/) e. _om )
59 1on 
 |-  1o e. On
60 59 a1i 
 |-  ( ( ph /\ W = (/) ) -> 1o e. On )
61 ovexd 
 |-  ( ph -> ( F supp (/) ) e. _V )
62 1 14 2 5 20 cantnfcl 
 |-  ( ph -> ( _E We ( F supp (/) ) /\ dom G e. _om ) )
63 62 simpld 
 |-  ( ph -> _E We ( F supp (/) ) )
64 5 oiiso 
 |-  ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
65 61 63 64 syl2anc 
 |-  ( ph -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
66 65 ad2antrr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
67 isof1o 
 |-  ( G Isom _E , _E ( dom G , ( F supp (/) ) ) -> G : dom G -1-1-onto-> ( F supp (/) ) )
68 66 67 syl 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> G : dom G -1-1-onto-> ( F supp (/) ) )
69 f1ocnv 
 |-  ( G : dom G -1-1-onto-> ( F supp (/) ) -> `' G : ( F supp (/) ) -1-1-onto-> dom G )
70 f1of 
 |-  ( `' G : ( F supp (/) ) -1-1-onto-> dom G -> `' G : ( F supp (/) ) --> dom G )
71 68 69 70 3syl 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> `' G : ( F supp (/) ) --> dom G )
72 ffvelcdm 
 |-  ( ( `' G : ( F supp (/) ) --> dom G /\ x e. ( F supp (/) ) ) -> ( `' G ` x ) e. dom G )
73 71 72 sylancom 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( `' G ` x ) e. dom G )
74 elssuni 
 |-  ( ( `' G ` x ) e. dom G -> ( `' G ` x ) C_ U. dom G )
75 73 74 syl 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( `' G ` x ) C_ U. dom G )
76 onelon 
 |-  ( ( dom G e. On /\ ( `' G ` x ) e. dom G ) -> ( `' G ` x ) e. On )
77 27 73 76 sylancr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( `' G ` x ) e. On )
78 onuni 
 |-  ( dom G e. On -> U. dom G e. On )
79 27 78 ax-mp 
 |-  U. dom G e. On
80 ontri1 
 |-  ( ( ( `' G ` x ) e. On /\ U. dom G e. On ) -> ( ( `' G ` x ) C_ U. dom G <-> -. U. dom G e. ( `' G ` x ) ) )
81 77 79 80 sylancl 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( ( `' G ` x ) C_ U. dom G <-> -. U. dom G e. ( `' G ` x ) ) )
82 75 81 mpbid 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> -. U. dom G e. ( `' G ` x ) )
83 35 ad2antrr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> U. dom G e. dom G )
84 isorel 
 |-  ( ( G Isom _E , _E ( dom G , ( F supp (/) ) ) /\ ( U. dom G e. dom G /\ ( `' G ` x ) e. dom G ) ) -> ( U. dom G _E ( `' G ` x ) <-> ( G ` U. dom G ) _E ( G ` ( `' G ` x ) ) ) )
85 66 83 73 84 syl12anc 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( U. dom G _E ( `' G ` x ) <-> ( G ` U. dom G ) _E ( G ` ( `' G ` x ) ) ) )
86 fvex 
 |-  ( `' G ` x ) e. _V
87 86 epeli 
 |-  ( U. dom G _E ( `' G ` x ) <-> U. dom G e. ( `' G ` x ) )
88 10 breq1i 
 |-  ( W _E ( G ` ( `' G ` x ) ) <-> ( G ` U. dom G ) _E ( G ` ( `' G ` x ) ) )
89 fvex 
 |-  ( G ` ( `' G ` x ) ) e. _V
90 89 epeli 
 |-  ( W _E ( G ` ( `' G ` x ) ) <-> W e. ( G ` ( `' G ` x ) ) )
91 88 90 bitr3i 
 |-  ( ( G ` U. dom G ) _E ( G ` ( `' G ` x ) ) <-> W e. ( G ` ( `' G ` x ) ) )
92 85 87 91 3bitr3g 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( U. dom G e. ( `' G ` x ) <-> W e. ( G ` ( `' G ` x ) ) ) )
93 simplr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> W = (/) )
94 f1ocnvfv2 
 |-  ( ( G : dom G -1-1-onto-> ( F supp (/) ) /\ x e. ( F supp (/) ) ) -> ( G ` ( `' G ` x ) ) = x )
95 68 94 sylancom 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( G ` ( `' G ` x ) ) = x )
96 93 95 eleq12d 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( W e. ( G ` ( `' G ` x ) ) <-> (/) e. x ) )
97 92 96 bitrd 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( U. dom G e. ( `' G ` x ) <-> (/) e. x ) )
98 82 97 mtbid 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> -. (/) e. x )
99 onss 
 |-  ( A e. On -> A C_ On )
100 2 99 syl 
 |-  ( ph -> A C_ On )
101 24 100 sstrd 
 |-  ( ph -> ( F supp (/) ) C_ On )
102 101 adantr 
 |-  ( ( ph /\ W = (/) ) -> ( F supp (/) ) C_ On )
103 102 sselda 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> x e. On )
104 on0eqel 
 |-  ( x e. On -> ( x = (/) \/ (/) e. x ) )
105 103 104 syl 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( x = (/) \/ (/) e. x ) )
106 105 ord 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> ( -. x = (/) -> (/) e. x ) )
107 98 106 mt3d 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> x = (/) )
108 el1o 
 |-  ( x e. 1o <-> x = (/) )
109 107 108 sylibr 
 |-  ( ( ( ph /\ W = (/) ) /\ x e. ( F supp (/) ) ) -> x e. 1o )
110 109 ex 
 |-  ( ( ph /\ W = (/) ) -> ( x e. ( F supp (/) ) -> x e. 1o ) )
111 110 ssrdv 
 |-  ( ( ph /\ W = (/) ) -> ( F supp (/) ) C_ 1o )
112 1 55 56 57 58 60 111 cantnflt2 
 |-  ( ( ph /\ W = (/) ) -> ( ( _om CNF A ) ` F ) e. ( _om ^o 1o ) )
113 oe1 
 |-  ( _om e. On -> ( _om ^o 1o ) = _om )
114 13 113 ax-mp 
 |-  ( _om ^o 1o ) = _om
115 112 114 eleqtrdi 
 |-  ( ( ph /\ W = (/) ) -> ( ( _om CNF A ) ` F ) e. _om )
116 54 115 eqeltrrd 
 |-  ( ( ph /\ W = (/) ) -> B e. _om )
117 116 ex 
 |-  ( ph -> ( W = (/) -> B e. _om ) )
118 117 necon3bd 
 |-  ( ph -> ( -. B e. _om -> W =/= (/) ) )
119 49 118 mpd 
 |-  ( ph -> W =/= (/) )
120 dif1o 
 |-  ( W e. ( On \ 1o ) <-> ( W e. On /\ W =/= (/) ) )
121 42 119 120 sylanbrc 
 |-  ( ph -> W e. ( On \ 1o ) )