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

Step	Hyp	Ref	Expression
1		f1of1	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A \underset{1-1}{⟶} B$
2		f1fveq	$⊢ (H : A \underset{1-1}{⟶} B \land (x \in A \land y \in A)) \to (H (x) = H (y) \leftrightarrow x = y)$
3	1 2	sylan	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to (H (x) = H (y) \leftrightarrow x = y)$
4		fvex	$⊢ H (y) \in V$
5	4	ideq	$⊢ H (x) I H (y) \leftrightarrow H (x) = H (y)$
6	5	a1i	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to (H (x) I H (y) \leftrightarrow H (x) = H (y))$
7		ideqg	$⊢ y \in A \to (x I y \leftrightarrow x = y)$
8	7	ad2antll	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to (x I y \leftrightarrow x = y)$
9	3 6 8	3bitr4rd	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to (x I y \leftrightarrow H (x) I H (y))$
10	9	ralrimivva	$⊢ H : A \underset{1-1 onto}{⟶} B \to \forall x \in A \forall y \in A (x I y \leftrightarrow H (x) I H (y))$
11	10	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 I y \leftrightarrow H (x) I H (y)))$
12		df-isom	$⊢ H {Isom}_{I, I} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x I y \leftrightarrow H (x) I H (y)))$
13	11 12	bitr4i	$⊢ H : A \underset{1-1 onto}{⟶} B \leftrightarrow H {Isom}_{I, I} (A, B)$

Metamath Proof Explorer