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 \underset{1-1 onto}{⟶} B \leftrightarrow H {Isom}_{V \times V, V \times V} (A, B)$

Proof

Step	Hyp	Ref	Expression
1		fvex	$⊢ H (x) \in V$
2		fvex	$⊢ H (y) \in V$
3	1 2	opelvv	$⊢ ⟨H (x), H (y)⟩ \in (V \times V)$
4		df-br	$⊢ H (x) (V \times V) H (y) \leftrightarrow ⟨H (x), H (y)⟩ \in (V \times V)$
5	3 4	mpbir	$⊢ H (x) (V \times V) H (y)$
6	5	a1i	$⊢ x (V \times V) y \to H (x) (V \times V) H (y)$
7		opelvvg	$⊢ (x \in A \land y \in A) \to ⟨x, y⟩ \in (V \times V)$
8		df-br	$⊢ x (V \times V) y \leftrightarrow ⟨x, y⟩ \in (V \times V)$
9	7 8	sylibr	$⊢ (x \in A \land y \in A) \to x (V \times V) y$
10	9	a1d	$⊢ (x \in A \land y \in A) \to (H (x) (V \times V) H (y) \to x (V \times V) y)$
11	6 10	impbid2	$⊢ (x \in A \land y \in A) \to (x (V \times V) y \leftrightarrow H (x) (V \times V) H (y))$
12	11	adantl	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to (x (V \times V) y \leftrightarrow H (x) (V \times V) H (y))$
13	12	ralrimivva	$⊢ H : A \underset{1-1 onto}{⟶} B \to \forall x \in A \forall y \in A (x (V \times V) y \leftrightarrow H (x) (V \times V) H (y))$
14	13	pm4.71i	$⊢ H : A \underset{1-1 onto}{⟶} B \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x (V \times V) y \leftrightarrow H (x) (V \times V) H (y)))$
15		df-isom	$⊢ H {Isom}_{V \times V, V \times V} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x (V \times V) y \leftrightarrow H (x) (V \times V) H (y)))$
16	14 15	bitr4i	$⊢ H : A \underset{1-1 onto}{⟶} B \leftrightarrow H {Isom}_{V \times V, V \times V} (A, B)$