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 eqtrid
 |-  ( 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 )