This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isof1oidb

Description: A function is a bijection iff it is an isomorphism regarding the identity relation. (Contributed by AV, 9-May-2021)

Ref Expression
Assertion isof1oidb 
|- ( H : A -1-1-onto-> B <-> H Isom _I , _I ( A , B ) )

Proof

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