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