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

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

Proof

Step Hyp Ref Expression
1 f1of1 ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 –1-1→ 𝐵 )
2 f1fveq ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
3 1 2 sylan ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
4 fvex ⊢ ( 𝐻 ‘ 𝑦 ) ∈ V
5 4 ideq ⊢ ( ( 𝐻 ‘ 𝑥 ) I ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) )
6 5 a1i ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) I ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) ) )
7 ideqg ⊢ ( 𝑦 ∈ 𝐴 → ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 ) )
8 7 ad2antll ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 ) )
9 3 6 8 3bitr4rd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 I 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) I ( 𝐻 ‘ 𝑦 ) ) )
10 9 ralrimivva ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 I 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) I ( 𝐻 ‘ 𝑦 ) ) )
11 10 pm4.71i ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 I 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) I ( 𝐻 ‘ 𝑦 ) ) ) )
12 df-isom ⊢ ( 𝐻 Isom I , I ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 I 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) I ( 𝐻 ‘ 𝑦 ) ) ) )
13 11 12 bitr4i ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ 𝐻 Isom I , I ( 𝐴 , 𝐵 ) )