This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ 𝐻 Isom ( V × V ) , ( V × V ) ( 𝐴 , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( 𝐻 ‘ 𝑥 ) ∈ V
2 fvex ⊢ ( 𝐻 ‘ 𝑦 ) ∈ V
3 1 2 opelvv ⊢ ⟨ ( 𝐻 ‘ 𝑥 ) , ( 𝐻 ‘ 𝑦 ) ⟩ ∈ ( V × V )
4 df-br ⊢ ( ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ↔ ⟨ ( 𝐻 ‘ 𝑥 ) , ( 𝐻 ‘ 𝑦 ) ⟩ ∈ ( V × V ) )
5 3 4 mpbir ⊢ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 )
6 5 a1i ⊢ ( 𝑥 ( V × V ) 𝑦 → ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) )
7 opelvvg ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V × V ) )
8 df-br ⊢ ( 𝑥 ( V × V ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V × V ) )
9 7 8 sylibr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ( V × V ) 𝑦 )
10 9 a1d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) → 𝑥 ( V × V ) 𝑦 ) )
11 6 10 impbid2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) )
12 11 adantl ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) )
13 12 ralrimivva ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) )
14 13 pm4.71i ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) ) )
15 df-isom ⊢ ( 𝐻 Isom ( V × V ) , ( V × V ) ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) ) )
16 14 15 bitr4i ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ 𝐻 Isom ( V × V ) , ( V × V ) ( 𝐴 , 𝐵 ) )