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 
|- 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 )
cnfcom2.1 
|- ( ph -> (/) e. B )
Assertion cnfcom2lem 
|- ( ph -> dom G = suc U. dom G )

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 cnfcom2.1 
 |-  ( ph -> (/) e. B )
12 n0i 
 |-  ( (/) e. B -> -. B = (/) )
13 11 12 syl 
 |-  ( ph -> -. B = (/) )
14 omelon 
 |-  _om e. On
15 14 a1i 
 |-  ( ph -> _om e. On )
16 1 15 2 cantnff1o 
 |-  ( ph -> ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) )
17 f1ocnv 
 |-  ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) -> `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S )
18 f1of 
 |-  ( `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
19 16 17 18 3syl 
 |-  ( ph -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
20 19 3 ffvelrnd 
 |-  ( ph -> ( `' ( _om CNF A ) ` B ) e. S )
21 4 20 eqeltrid 
 |-  ( ph -> F e. S )
22 1 15 2 cantnfs 
 |-  ( ph -> ( F e. S <-> ( F : A --> _om /\ F finSupp (/) ) ) )
23 21 22 mpbid 
 |-  ( ph -> ( F : A --> _om /\ F finSupp (/) ) )
24 23 simpld 
 |-  ( ph -> F : A --> _om )
25 24 adantr 
 |-  ( ( ph /\ dom G = (/) ) -> F : A --> _om )
26 25 feqmptd 
 |-  ( ( ph /\ dom G = (/) ) -> F = ( x e. A |-> ( F ` x ) ) )
27 dif0 
 |-  ( A \ (/) ) = A
28 27 eleq2i 
 |-  ( x e. ( A \ (/) ) <-> x e. A )
29 simpr 
 |-  ( ( ph /\ dom G = (/) ) -> dom G = (/) )
30 ovexd 
 |-  ( ph -> ( F supp (/) ) e. _V )
31 1 15 2 5 21 cantnfcl 
 |-  ( ph -> ( _E We ( F supp (/) ) /\ dom G e. _om ) )
32 31 simpld 
 |-  ( ph -> _E We ( F supp (/) ) )
33 5 oien 
 |-  ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> dom G ~~ ( F supp (/) ) )
34 30 32 33 syl2anc 
 |-  ( ph -> dom G ~~ ( F supp (/) ) )
35 34 adantr 
 |-  ( ( ph /\ dom G = (/) ) -> dom G ~~ ( F supp (/) ) )
36 29 35 eqbrtrrd 
 |-  ( ( ph /\ dom G = (/) ) -> (/) ~~ ( F supp (/) ) )
37 36 ensymd 
 |-  ( ( ph /\ dom G = (/) ) -> ( F supp (/) ) ~~ (/) )
38 en0 
 |-  ( ( F supp (/) ) ~~ (/) <-> ( F supp (/) ) = (/) )
39 37 38 sylib 
 |-  ( ( ph /\ dom G = (/) ) -> ( F supp (/) ) = (/) )
40 ss0b 
 |-  ( ( F supp (/) ) C_ (/) <-> ( F supp (/) ) = (/) )
41 39 40 sylibr 
 |-  ( ( ph /\ dom G = (/) ) -> ( F supp (/) ) C_ (/) )
42 2 adantr 
 |-  ( ( ph /\ dom G = (/) ) -> A e. On )
43 0ex 
 |-  (/) e. _V
44 43 a1i 
 |-  ( ( ph /\ dom G = (/) ) -> (/) e. _V )
45 25 41 42 44 suppssr 
 |-  ( ( ( ph /\ dom G = (/) ) /\ x e. ( A \ (/) ) ) -> ( F ` x ) = (/) )
46 28 45 sylan2br 
 |-  ( ( ( ph /\ dom G = (/) ) /\ x e. A ) -> ( F ` x ) = (/) )
47 46 mpteq2dva 
 |-  ( ( ph /\ dom G = (/) ) -> ( x e. A |-> ( F ` x ) ) = ( x e. A |-> (/) ) )
48 26 47 eqtrd 
 |-  ( ( ph /\ dom G = (/) ) -> F = ( x e. A |-> (/) ) )
49 fconstmpt 
 |-  ( A X. { (/) } ) = ( x e. A |-> (/) )
50 48 49 eqtr4di 
 |-  ( ( ph /\ dom G = (/) ) -> F = ( A X. { (/) } ) )
51 50 fveq2d 
 |-  ( ( ph /\ dom G = (/) ) -> ( ( _om CNF A ) ` F ) = ( ( _om CNF A ) ` ( A X. { (/) } ) ) )
52 4 fveq2i 
 |-  ( ( _om CNF A ) ` F ) = ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) )
53 f1ocnvfv2 
 |-  ( ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) /\ B e. ( _om ^o A ) ) -> ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) = B )
54 16 3 53 syl2anc 
 |-  ( ph -> ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) = B )
55 52 54 syl5eq 
 |-  ( ph -> ( ( _om CNF A ) ` F ) = B )
56 55 adantr 
 |-  ( ( ph /\ dom G = (/) ) -> ( ( _om CNF A ) ` F ) = B )
57 peano1 
 |-  (/) e. _om
58 57 a1i 
 |-  ( ph -> (/) e. _om )
59 1 15 2 58 cantnf0 
 |-  ( ph -> ( ( _om CNF A ) ` ( A X. { (/) } ) ) = (/) )
60 59 adantr 
 |-  ( ( ph /\ dom G = (/) ) -> ( ( _om CNF A ) ` ( A X. { (/) } ) ) = (/) )
61 51 56 60 3eqtr3d 
 |-  ( ( ph /\ dom G = (/) ) -> B = (/) )
62 13 61 mtand 
 |-  ( ph -> -. dom G = (/) )
63 nnlim 
 |-  ( dom G e. _om -> -. Lim dom G )
64 31 63 simpl2im 
 |-  ( ph -> -. Lim dom G )
65 ioran 
 |-  ( -. ( dom G = (/) \/ Lim dom G ) <-> ( -. dom G = (/) /\ -. Lim dom G ) )
66 62 64 65 sylanbrc 
 |-  ( ph -> -. ( dom G = (/) \/ Lim dom G ) )
67 5 oicl 
 |-  Ord dom G
68 unizlim 
 |-  ( Ord dom G -> ( dom G = U. dom G <-> ( dom G = (/) \/ Lim dom G ) ) )
69 67 68 ax-mp 
 |-  ( dom G = U. dom G <-> ( dom G = (/) \/ Lim dom G ) )
70 66 69 sylnibr 
 |-  ( ph -> -. dom G = U. dom G )
71 orduniorsuc 
 |-  ( Ord dom G -> ( dom G = U. dom G \/ dom G = suc U. dom G ) )
72 67 71 mp1i 
 |-  ( ph -> ( dom G = U. dom G \/ dom G = suc U. dom G ) )
73 72 ord 
 |-  ( ph -> ( -. dom G = U. dom G -> dom G = suc U. dom G ) )
74 70 73 mpd 
 |-  ( ph -> dom G = suc U. dom G )