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