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

Metamath Proof Explorer

Theorem f1ocnvfvrneq

Description: If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017)

Ref Expression
Assertion f1ocnvfvrneq ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 f1f1orn ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
2 f1ocnv ⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 → ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝐴 )
3 f1of1 ⊢ ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝐴 → ◡ 𝐹 : ran 𝐹 –1-1→ 𝐴 )
4 f1veqaeq ⊢ ( ( ◡ 𝐹 : ran 𝐹 –1-1→ 𝐴 ∧ ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) )
5 4 ex ⊢ ( ◡ 𝐹 : ran 𝐹 –1-1→ 𝐴 → ( ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) ) )
6 1 2 3 5 4syl ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) ) )
7 6 imp ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹 ) ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = ( ◡ 𝐹 ‘ 𝐷 ) → 𝐶 = 𝐷 ) )