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 ) ( 𝐴 , 𝐵 ) )