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 × V , V × V A B

Proof

Step Hyp Ref Expression
1 fvex ⊢ H ⁡ x ∈ V
2 fvex ⊢ H ⁡ y ∈ V
3 1 2 opelvv ⊢ H ⁡ x H ⁡ y ∈ V × V
4 df-br ⊢ H ⁡ x V × V H ⁡ y ↔ H ⁡ x H ⁡ y ∈ V × V
5 3 4 mpbir ⊢ H ⁡ x V × V H ⁡ y
6 5 a1i ⊢ x V × V y → H ⁡ x V × V H ⁡ y
7 opelvvg ⊢ x ∈ A ∧ y ∈ A → x y ∈ V × V
8 df-br ⊢ x V × V y ↔ x y ∈ V × V
9 7 8 sylibr ⊢ x ∈ A ∧ y ∈ A → x V × V y
10 9 a1d ⊢ x ∈ A ∧ y ∈ A → H ⁡ x V × V H ⁡ y → x V × V y
11 6 10 impbid2 ⊢ x ∈ A ∧ y ∈ A → x V × V y ↔ H ⁡ x V × V H ⁡ y
12 11 adantl ⊢ H : A ⟶ 1-1 onto B ∧ x ∈ A ∧ y ∈ A → x V × V y ↔ H ⁡ x V × V H ⁡ y
13 12 ralrimivva ⊢ H : A ⟶ 1-1 onto B → ∀ x ∈ A ∀ y ∈ A x V × V y ↔ H ⁡ x V × V H ⁡ y
14 13 pm4.71i ⊢ H : A ⟶ 1-1 onto B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x V × V y ↔ H ⁡ x V × V H ⁡ y
15 df-isom ⊢ H Isom V × V , V × V A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x V × V y ↔ H ⁡ x V × V H ⁡ y
16 14 15 bitr4i ⊢ H : A ⟶ 1-1 onto B ↔ H Isom V × V , V × V A B