Metamath Proof Explorer

Theorem cnfcom3clem

Description: Lemma for cnfcom3c . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 4-Jul-2019)

Ref Expression
Hypotheses cnfcom3c.s 
|- S = dom ( _om CNF A )
cnfcom3c.f 
|- F = ( `' ( _om CNF A ) ` b )
cnfcom3c.g 
|- G = OrdIso ( _E , ( F supp (/) ) )
cnfcom3c.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )
cnfcom3c.t 
|- T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) )
cnfcom3c.m 
|- M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )
cnfcom3c.k 
|- K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )
cnfcom3c.w 
|- W = ( G ` U. dom G )
cnfcom3c.x 
|- X = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( F ` W ) .o v ) +o u ) )
cnfcom3c.y 
|- Y = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o u ) +o v ) )
cnfcom3c.n 
|- N = ( ( X o. `' Y ) o. ( T ` dom G ) )
cnfcom3c.l 
|- L = ( b e. ( _om ^o A ) |-> N )
Assertion cnfcom3clem 
|- ( A e. On -> E. g A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) )

Proof

Step Hyp Ref Expression
1 cnfcom3c.s 
 |-  S = dom ( _om CNF A )
2 cnfcom3c.f 
 |-  F = ( `' ( _om CNF A ) ` b )
3 cnfcom3c.g 
 |-  G = OrdIso ( _E , ( F supp (/) ) )
4 cnfcom3c.h 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )
5 cnfcom3c.t 
 |-  T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) )
6 cnfcom3c.m 
 |-  M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )
7 cnfcom3c.k 
 |-  K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )
8 cnfcom3c.w 
 |-  W = ( G ` U. dom G )
9 cnfcom3c.x 
 |-  X = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( F ` W ) .o v ) +o u ) )
10 cnfcom3c.y 
 |-  Y = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o u ) +o v ) )
11 cnfcom3c.n 
 |-  N = ( ( X o. `' Y ) o. ( T ` dom G ) )
12 cnfcom3c.l 
 |-  L = ( b e. ( _om ^o A ) |-> N )
13 simp1 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> A e. On )
14 omelon 
 |-  _om e. On
15 1onn 
 |-  1o e. _om
16 ondif2 
 |-  ( _om e. ( On \ 2o ) <-> ( _om e. On /\ 1o e. _om ) )
17 14 15 16 mpbir2an 
 |-  _om e. ( On \ 2o )
18 oeworde 
 |-  ( ( _om e. ( On \ 2o ) /\ A e. On ) -> A C_ ( _om ^o A ) )
19 17 13 18 sylancr 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> A C_ ( _om ^o A ) )
20 simp2 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> b e. A )
21 19 20 sseldd 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> b e. ( _om ^o A ) )
22 simp3 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> _om C_ b )
23 1 13 21 2 3 4 5 6 7 8 22 cnfcom3lem 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> W e. ( On \ 1o ) )
24 1 13 21 2 3 4 5 6 7 8 22 9 10 11 cnfcom3 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> N : b -1-1-onto-> ( _om ^o W ) )
25 f1of 
 |-  ( N : b -1-1-onto-> ( _om ^o W ) -> N : b --> ( _om ^o W ) )
26 24 25 syl 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> N : b --> ( _om ^o W ) )
27 26 20 fexd 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> N e. _V )
28 12 fvmpt2 
 |-  ( ( b e. ( _om ^o A ) /\ N e. _V ) -> ( L ` b ) = N )
29 21 27 28 syl2anc 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> ( L ` b ) = N )
30 29 f1oeq1d 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> ( ( L ` b ) : b -1-1-onto-> ( _om ^o W ) <-> N : b -1-1-onto-> ( _om ^o W ) ) )
31 24 30 mpbird 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> ( L ` b ) : b -1-1-onto-> ( _om ^o W ) )
32 oveq2 
 |-  ( w = W -> ( _om ^o w ) = ( _om ^o W ) )
33 32 f1oeq3d 
 |-  ( w = W -> ( ( L ` b ) : b -1-1-onto-> ( _om ^o w ) <-> ( L ` b ) : b -1-1-onto-> ( _om ^o W ) ) )
34 33 rspcev 
 |-  ( ( W e. ( On \ 1o ) /\ ( L ` b ) : b -1-1-onto-> ( _om ^o W ) ) -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) )
35 23 31 34 syl2anc 
 |-  ( ( A e. On /\ b e. A /\ _om C_ b ) -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) )
36 35 3expia 
 |-  ( ( A e. On /\ b e. A ) -> ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
37 36 ralrimiva 
 |-  ( A e. On -> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
38 ovex 
 |-  ( _om ^o A ) e. _V
39 38 mptex 
 |-  ( b e. ( _om ^o A ) |-> N ) e. _V
40 12 39 eqeltri 
 |-  L e. _V
41 nfmpt1 
 |-  F/_ b ( b e. ( _om ^o A ) |-> N )
42 12 41 nfcxfr 
 |-  F/_ b L
43 42 nfeq2 
 |-  F/ b g = L
44 fveq1 
 |-  ( g = L -> ( g ` b ) = ( L ` b ) )
45 44 f1oeq1d 
 |-  ( g = L -> ( ( g ` b ) : b -1-1-onto-> ( _om ^o w ) <-> ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
46 45 rexbidv 
 |-  ( g = L -> ( E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) <-> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
47 46 imbi2d 
 |-  ( g = L -> ( ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) <-> ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) )
48 43 47 ralbid 
 |-  ( g = L -> ( A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) <-> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) )
49 40 48 spcev 
 |-  ( A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( L ` b ) : b -1-1-onto-> ( _om ^o w ) ) -> E. g A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
50 37 49 syl 
 |-  ( A e. On -> E. g A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) )