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