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 ∈ A ∧ y ∈ A → H ⁡ x = H ⁡ y ↔ x = y
3 1 2 sylan ⊢ H : A ⟶ 1-1 onto B ∧ x ∈ A ∧ y ∈ A → H ⁡ x = H ⁡ y ↔ x = y
4 fvex ⊢ H ⁡ y ∈ V
5 4 ideq ⊢ H ⁡ x I H ⁡ y ↔ H ⁡ x = H ⁡ y
6 5 a1i ⊢ H : A ⟶ 1-1 onto B ∧ x ∈ A ∧ y ∈ A → H ⁡ x I H ⁡ y ↔ H ⁡ x = H ⁡ y
7 ideqg ⊢ y ∈ A → x I y ↔ x = y
8 7 ad2antll ⊢ H : A ⟶ 1-1 onto B ∧ x ∈ A ∧ y ∈ A → x I y ↔ x = y
9 3 6 8 3bitr4rd ⊢ H : A ⟶ 1-1 onto B ∧ x ∈ A ∧ y ∈ A → x I y ↔ H ⁡ x I H ⁡ y
10 9 ralrimivva ⊢ H : A ⟶ 1-1 onto B → ∀ x ∈ A ∀ y ∈ 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 ∧ ∀ x ∈ A ∀ y ∈ A x I y ↔ H ⁡ x I H ⁡ y
12 df-isom ⊢ H Isom I , I A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ 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