Metamath Proof Explorer

Theorem infxpenc2

Description: Existence form of infxpenc . A "uniform" or "canonical" version of infxpen , asserting the existence of a single function g that simultaneously demonstrates product idempotence of all ordinals below a given bound. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Assertion infxpenc2 
|- ( A e. On -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) )

Proof

Step Hyp Ref Expression
1 cnfcom3c 
 |-  ( A e. On -> E. n A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) )
2 df-2o 
 |-  2o = suc 1o
3 2 oveq2i 
 |-  ( _om ^o 2o ) = ( _om ^o suc 1o )
4 omelon 
 |-  _om e. On
5 1on 
 |-  1o e. On
6 oesuc 
 |-  ( ( _om e. On /\ 1o e. On ) -> ( _om ^o suc 1o ) = ( ( _om ^o 1o ) .o _om ) )
7 4 5 6 mp2an 
 |-  ( _om ^o suc 1o ) = ( ( _om ^o 1o ) .o _om )
8 oe1 
 |-  ( _om e. On -> ( _om ^o 1o ) = _om )
9 4 8 ax-mp 
 |-  ( _om ^o 1o ) = _om
10 9 oveq1i 
 |-  ( ( _om ^o 1o ) .o _om ) = ( _om .o _om )
11 3 7 10 3eqtri 
 |-  ( _om ^o 2o ) = ( _om .o _om )
12 omxpen 
 |-  ( ( _om e. On /\ _om e. On ) -> ( _om .o _om ) ~~ ( _om X. _om ) )
13 4 4 12 mp2an 
 |-  ( _om .o _om ) ~~ ( _om X. _om )
14 11 13 eqbrtri 
 |-  ( _om ^o 2o ) ~~ ( _om X. _om )
15 xpomen 
 |-  ( _om X. _om ) ~~ _om
16 14 15 entri 
 |-  ( _om ^o 2o ) ~~ _om
17 16 a1i 
 |-  ( A e. On -> ( _om ^o 2o ) ~~ _om )
18 bren 
 |-  ( ( _om ^o 2o ) ~~ _om <-> E. f f : ( _om ^o 2o ) -1-1-onto-> _om )
19 17 18 sylib 
 |-  ( A e. On -> E. f f : ( _om ^o 2o ) -1-1-onto-> _om )
20 exdistrv 
 |-  ( E. n E. f ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) <-> ( E. n A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ E. f f : ( _om ^o 2o ) -1-1-onto-> _om ) )
21 simpl 
 |-  ( ( A e. On /\ ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) ) -> A e. On )
22 simprl 
 |-  ( ( A e. On /\ ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) ) -> A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) )
23 sseq2 
 |-  ( x = b -> ( _om C_ x <-> _om C_ b ) )
24 oveq2 
 |-  ( y = w -> ( _om ^o y ) = ( _om ^o w ) )
25 24 f1oeq3d 
 |-  ( y = w -> ( ( n ` x ) : x -1-1-onto-> ( _om ^o y ) <-> ( n ` x ) : x -1-1-onto-> ( _om ^o w ) ) )
26 25 cbvrexvw 
 |-  ( E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) <-> E. w e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o w ) )
27 fveq2 
 |-  ( x = b -> ( n ` x ) = ( n ` b ) )
28 27 f1oeq1d 
 |-  ( x = b -> ( ( n ` x ) : x -1-1-onto-> ( _om ^o w ) <-> ( n ` b ) : x -1-1-onto-> ( _om ^o w ) ) )
29 f1oeq2 
 |-  ( x = b -> ( ( n ` b ) : x -1-1-onto-> ( _om ^o w ) <-> ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
30 28 29 bitrd 
 |-  ( x = b -> ( ( n ` x ) : x -1-1-onto-> ( _om ^o w ) <-> ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
31 30 rexbidv 
 |-  ( x = b -> ( E. w e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o w ) <-> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
32 26 31 bitrid 
 |-  ( x = b -> ( E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) <-> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
33 23 32 imbi12d 
 |-  ( x = b -> ( ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) <-> ( _om C_ b -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) ) )
34 33 cbvralvw 
 |-  ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) <-> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
35 22 34 sylib 
 |-  ( ( A e. On /\ ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) ) -> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
36 oveq2 
 |-  ( b = z -> ( _om ^o b ) = ( _om ^o z ) )
37 36 cbvmptv 
 |-  ( b e. ( On \ 1o ) |-> ( _om ^o b ) ) = ( z e. ( On \ 1o ) |-> ( _om ^o z ) )
38 37 cnveqi 
 |-  `' ( b e. ( On \ 1o ) |-> ( _om ^o b ) ) = `' ( z e. ( On \ 1o ) |-> ( _om ^o z ) )
39 38 fveq1i 
 |-  ( `' ( b e. ( On \ 1o ) |-> ( _om ^o b ) ) ` ran ( n ` b ) ) = ( `' ( z e. ( On \ 1o ) |-> ( _om ^o z ) ) ` ran ( n ` b ) )
40 2on 
 |-  2o e. On
41 peano1 
 |-  (/) e. _om
42 oen0 
 |-  ( ( ( _om e. On /\ 2o e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o 2o ) )
43 41 42 mpan2 
 |-  ( ( _om e. On /\ 2o e. On ) -> (/) e. ( _om ^o 2o ) )
44 4 40 43 mp2an 
 |-  (/) e. ( _om ^o 2o )
45 eqid 
 |-  ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) ) = ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) )
46 45 fveqf1o 
 |-  ( ( f : ( _om ^o 2o ) -1-1-onto-> _om /\ (/) e. ( _om ^o 2o ) /\ (/) e. _om ) -> ( ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) ) : ( _om ^o 2o ) -1-1-onto-> _om /\ ( ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) ) ` (/) ) = (/) ) )
47 44 41 46 mp3an23 
 |-  ( f : ( _om ^o 2o ) -1-1-onto-> _om -> ( ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) ) : ( _om ^o 2o ) -1-1-onto-> _om /\ ( ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) ) ` (/) ) = (/) ) )
48 47 ad2antll 
 |-  ( ( A e. On /\ ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) ) -> ( ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) ) : ( _om ^o 2o ) -1-1-onto-> _om /\ ( ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) ) ` (/) ) = (/) ) )
49 48 simpld 
 |-  ( ( A e. On /\ ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) ) -> ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) ) : ( _om ^o 2o ) -1-1-onto-> _om )
50 48 simprd 
 |-  ( ( A e. On /\ ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) ) -> ( ( f o. ( ( _I |` ( ( _om ^o 2o ) \ { (/) , ( `' f ` (/) ) } ) ) u. { <. (/) , ( `' f ` (/) ) >. , <. ( `' f ` (/) ) , (/) >. } ) ) ` (/) ) = (/) )
51 21 35 39 49 50 infxpenc2lem3 
 |-  ( ( A e. On /\ ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) ) -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) )
52 51 ex 
 |-  ( A e. On -> ( ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) ) )
53 52 exlimdvv 
 |-  ( A e. On -> ( E. n E. f ( A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ f : ( _om ^o 2o ) -1-1-onto-> _om ) -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) ) )
54 20 53 biimtrrid 
 |-  ( A e. On -> ( ( E. n A. x e. A ( _om C_ x -> E. y e. ( On \ 1o ) ( n ` x ) : x -1-1-onto-> ( _om ^o y ) ) /\ E. f f : ( _om ^o 2o ) -1-1-onto-> _om ) -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) ) )
55 1 19 54 mp2and 
 |-  ( A e. On -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) )