Step |
Hyp |
Ref |
Expression |
1 |
|
f1of1 |
|- ( H : A -1-1-onto-> B -> H : A -1-1-> B ) |
2 |
|
f1fveq |
|- ( ( H : A -1-1-> B /\ ( x e. A /\ y e. A ) ) -> ( ( H ` x ) = ( H ` y ) <-> x = y ) ) |
3 |
1 2
|
sylan |
|- ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( ( H ` x ) = ( H ` y ) <-> x = y ) ) |
4 |
|
fvex |
|- ( H ` y ) e. _V |
5 |
4
|
ideq |
|- ( ( H ` x ) _I ( H ` y ) <-> ( H ` x ) = ( H ` y ) ) |
6 |
5
|
a1i |
|- ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( ( H ` x ) _I ( H ` y ) <-> ( H ` x ) = ( H ` y ) ) ) |
7 |
|
ideqg |
|- ( y e. A -> ( x _I y <-> x = y ) ) |
8 |
7
|
ad2antll |
|- ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( x _I y <-> x = y ) ) |
9 |
3 6 8
|
3bitr4rd |
|- ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( x _I y <-> ( H ` x ) _I ( H ` y ) ) ) |
10 |
9
|
ralrimivva |
|- ( H : A -1-1-onto-> B -> A. x e. A A. y e. A ( x _I y <-> ( H ` x ) _I ( H ` y ) ) ) |
11 |
10
|
pm4.71i |
|- ( H : A -1-1-onto-> B <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x _I y <-> ( H ` x ) _I ( H ` y ) ) ) ) |
12 |
|
df-isom |
|- ( H Isom _I , _I ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x _I y <-> ( H ` x ) _I ( H ` y ) ) ) ) |
13 |
11 12
|
bitr4i |
|- ( H : A -1-1-onto-> B <-> H Isom _I , _I ( A , B ) ) |