Metamath Proof Explorer

Theorem infxpenc2lem1

Description: Lemma for infxpenc2 . (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses infxpenc2.1 
|- ( ph -> A e. On )
infxpenc2.2 
|- ( ph -> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
infxpenc2.3 
|- W = ( `' ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` ran ( n ` b ) )
Assertion infxpenc2lem1 
|- ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( W e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o W ) ) )

Proof

Step Hyp Ref Expression
1 infxpenc2.1 
 |-  ( ph -> A e. On )
2 infxpenc2.2 
 |-  ( ph -> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
3 infxpenc2.3 
 |-  W = ( `' ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` ran ( n ` b ) )
4 2 r19.21bi 
 |-  ( ( ph /\ b e. A ) -> ( _om C_ b -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
5 4 impr 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) )
6 simpr 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
7 oveq2 
 |-  ( x = w -> ( _om ^o x ) = ( _om ^o w ) )
8 eqid 
 |-  ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) = ( x e. ( On \ 1o ) |-> ( _om ^o x ) )
9 ovex 
 |-  ( _om ^o w ) e. _V
10 7 8 9 fvmpt 
 |-  ( w e. ( On \ 1o ) -> ( ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` w ) = ( _om ^o w ) )
11 10 ad2antrl 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` w ) = ( _om ^o w ) )
12 f1ofo 
 |-  ( ( n ` b ) : b -1-1-onto-> ( _om ^o w ) -> ( n ` b ) : b -onto-> ( _om ^o w ) )
13 12 ad2antll 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( n ` b ) : b -onto-> ( _om ^o w ) )
14 forn 
 |-  ( ( n ` b ) : b -onto-> ( _om ^o w ) -> ran ( n ` b ) = ( _om ^o w ) )
15 13 14 syl 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ran ( n ` b ) = ( _om ^o w ) )
16 11 15 eqtr4d 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` w ) = ran ( n ` b ) )
17 ovex 
 |-  ( _om ^o x ) e. _V
18 17 2a1i 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( x e. ( On \ 1o ) -> ( _om ^o x ) e. _V ) )
19 omelon 
 |-  _om e. On
20 1onn 
 |-  1o e. _om
21 ondif2 
 |-  ( _om e. ( On \ 2o ) <-> ( _om e. On /\ 1o e. _om ) )
22 19 20 21 mpbir2an 
 |-  _om e. ( On \ 2o )
23 eldifi 
 |-  ( x e. ( On \ 1o ) -> x e. On )
24 23 ad2antrl 
 |-  ( ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) /\ ( x e. ( On \ 1o ) /\ y e. ( On \ 1o ) ) ) -> x e. On )
25 eldifi 
 |-  ( y e. ( On \ 1o ) -> y e. On )
26 25 ad2antll 
 |-  ( ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) /\ ( x e. ( On \ 1o ) /\ y e. ( On \ 1o ) ) ) -> y e. On )
27 oecan 
 |-  ( ( _om e. ( On \ 2o ) /\ x e. On /\ y e. On ) -> ( ( _om ^o x ) = ( _om ^o y ) <-> x = y ) )
28 22 24 26 27 mp3an2i 
 |-  ( ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) /\ ( x e. ( On \ 1o ) /\ y e. ( On \ 1o ) ) ) -> ( ( _om ^o x ) = ( _om ^o y ) <-> x = y ) )
29 28 ex 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( ( x e. ( On \ 1o ) /\ y e. ( On \ 1o ) ) -> ( ( _om ^o x ) = ( _om ^o y ) <-> x = y ) ) )
30 18 29 dom2lem 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) : ( On \ 1o ) -1-1-> _V )
31 f1f1orn 
 |-  ( ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) : ( On \ 1o ) -1-1-> _V -> ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) : ( On \ 1o ) -1-1-onto-> ran ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) )
32 30 31 syl 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) : ( On \ 1o ) -1-1-onto-> ran ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) )
33 simprl 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> w e. ( On \ 1o ) )
34 f1ocnvfv 
 |-  ( ( ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) : ( On \ 1o ) -1-1-onto-> ran ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) /\ w e. ( On \ 1o ) ) -> ( ( ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` w ) = ran ( n ` b ) -> ( `' ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` ran ( n ` b ) ) = w ) )
35 32 33 34 syl2anc 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( ( ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` w ) = ran ( n ` b ) -> ( `' ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` ran ( n ` b ) ) = w ) )
36 16 35 mpd 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( `' ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` ran ( n ` b ) ) = w )
37 3 36 eqtrid 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> W = w )
38 37 eleq1d 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( W e. ( On \ 1o ) <-> w e. ( On \ 1o ) ) )
39 37 oveq2d 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( _om ^o W ) = ( _om ^o w ) )
40 39 f1oeq3d 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( ( n ` b ) : b -1-1-onto-> ( _om ^o W ) <-> ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
41 38 40 anbi12d 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( ( W e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o W ) ) <-> ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) )
42 6 41 mpbird 
 |-  ( ( ( ph /\ ( b e. A /\ _om C_ b ) ) /\ ( w e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) -> ( W e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o W ) ) )
43 5 42 rexlimddv 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( W e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o W ) ) )