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