| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fin1a2lem.b |
|- E = ( x e. _om |-> ( 2o .o x ) ) |
| 2 |
|
2onn |
|- 2o e. _om |
| 3 |
|
nnmcl |
|- ( ( 2o e. _om /\ x e. _om ) -> ( 2o .o x ) e. _om ) |
| 4 |
2 3
|
mpan |
|- ( x e. _om -> ( 2o .o x ) e. _om ) |
| 5 |
1 4
|
fmpti |
|- E : _om --> _om |
| 6 |
1
|
fin1a2lem3 |
|- ( a e. _om -> ( E ` a ) = ( 2o .o a ) ) |
| 7 |
1
|
fin1a2lem3 |
|- ( b e. _om -> ( E ` b ) = ( 2o .o b ) ) |
| 8 |
6 7
|
eqeqan12d |
|- ( ( a e. _om /\ b e. _om ) -> ( ( E ` a ) = ( E ` b ) <-> ( 2o .o a ) = ( 2o .o b ) ) ) |
| 9 |
|
2on |
|- 2o e. On |
| 10 |
9
|
a1i |
|- ( ( a e. _om /\ b e. _om ) -> 2o e. On ) |
| 11 |
|
nnon |
|- ( a e. _om -> a e. On ) |
| 12 |
11
|
adantr |
|- ( ( a e. _om /\ b e. _om ) -> a e. On ) |
| 13 |
|
nnon |
|- ( b e. _om -> b e. On ) |
| 14 |
13
|
adantl |
|- ( ( a e. _om /\ b e. _om ) -> b e. On ) |
| 15 |
|
0lt1o |
|- (/) e. 1o |
| 16 |
|
elelsuc |
|- ( (/) e. 1o -> (/) e. suc 1o ) |
| 17 |
15 16
|
ax-mp |
|- (/) e. suc 1o |
| 18 |
|
df-2o |
|- 2o = suc 1o |
| 19 |
17 18
|
eleqtrri |
|- (/) e. 2o |
| 20 |
19
|
a1i |
|- ( ( a e. _om /\ b e. _om ) -> (/) e. 2o ) |
| 21 |
|
omcan |
|- ( ( ( 2o e. On /\ a e. On /\ b e. On ) /\ (/) e. 2o ) -> ( ( 2o .o a ) = ( 2o .o b ) <-> a = b ) ) |
| 22 |
10 12 14 20 21
|
syl31anc |
|- ( ( a e. _om /\ b e. _om ) -> ( ( 2o .o a ) = ( 2o .o b ) <-> a = b ) ) |
| 23 |
8 22
|
bitrd |
|- ( ( a e. _om /\ b e. _om ) -> ( ( E ` a ) = ( E ` b ) <-> a = b ) ) |
| 24 |
23
|
biimpd |
|- ( ( a e. _om /\ b e. _om ) -> ( ( E ` a ) = ( E ` b ) -> a = b ) ) |
| 25 |
24
|
rgen2 |
|- A. a e. _om A. b e. _om ( ( E ` a ) = ( E ` b ) -> a = b ) |
| 26 |
|
dff13 |
|- ( E : _om -1-1-> _om <-> ( E : _om --> _om /\ A. a e. _om A. b e. _om ( ( E ` a ) = ( E ` b ) -> a = b ) ) ) |
| 27 |
5 25 26
|
mpbir2an |
|- E : _om -1-1-> _om |