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 syl5bb
 |-  ( 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 syl5bir
 |-  ( 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 ) )