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

Metamath Proof Explorer

Theorem isof1oopb

Description: A function is a bijection iff it is an isomorphism regarding the universal class of ordered pairs as relations. (Contributed by AV, 9-May-2021)

Ref Expression
Assertion isof1oopb 
|- ( H : A -1-1-onto-> B <-> H Isom ( _V X. _V ) , ( _V X. _V ) ( A , B ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( H ` x ) e. _V
2 fvex 
 |-  ( H ` y ) e. _V
3 1 2 opelvv 
 |-  <. ( H ` x ) , ( H ` y ) >. e. ( _V X. _V )
4 df-br 
 |-  ( ( H ` x ) ( _V X. _V ) ( H ` y ) <-> <. ( H ` x ) , ( H ` y ) >. e. ( _V X. _V ) )
5 3 4 mpbir 
 |-  ( H ` x ) ( _V X. _V ) ( H ` y )
6 5 a1i 
 |-  ( x ( _V X. _V ) y -> ( H ` x ) ( _V X. _V ) ( H ` y ) )
7 opelvvg 
 |-  ( ( x e. A /\ y e. A ) -> <. x , y >. e. ( _V X. _V ) )
8 df-br 
 |-  ( x ( _V X. _V ) y <-> <. x , y >. e. ( _V X. _V ) )
9 7 8 sylibr 
 |-  ( ( x e. A /\ y e. A ) -> x ( _V X. _V ) y )
10 9 a1d 
 |-  ( ( x e. A /\ y e. A ) -> ( ( H ` x ) ( _V X. _V ) ( H ` y ) -> x ( _V X. _V ) y ) )
11 6 10 impbid2 
 |-  ( ( x e. A /\ y e. A ) -> ( x ( _V X. _V ) y <-> ( H ` x ) ( _V X. _V ) ( H ` y ) ) )
12 11 adantl 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( x ( _V X. _V ) y <-> ( H ` x ) ( _V X. _V ) ( H ` y ) ) )
13 12 ralrimivva 
 |-  ( H : A -1-1-onto-> B -> A. x e. A A. y e. A ( x ( _V X. _V ) y <-> ( H ` x ) ( _V X. _V ) ( H ` y ) ) )
14 13 pm4.71i 
 |-  ( H : A -1-1-onto-> B <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x ( _V X. _V ) y <-> ( H ` x ) ( _V X. _V ) ( H ` y ) ) ) )
15 df-isom 
 |-  ( H Isom ( _V X. _V ) , ( _V X. _V ) ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x ( _V X. _V ) y <-> ( H ` x ) ( _V X. _V ) ( H ` y ) ) ) )
16 14 15 bitr4i 
 |-  ( H : A -1-1-onto-> B <-> H Isom ( _V X. _V ) , ( _V X. _V ) ( A , B ) )