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	$⊢ (F : A \underset{1-1}{⟶} B \land (C \in ran F \land D \in ran F)) \to (F^{-1} (C) = F^{-1} (D) \to C = D)$

Proof

Step	Hyp	Ref	Expression
1		f1f1orn	$⊢ F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} ran F$
2		f1ocnv	$⊢ F : A \underset{1-1 onto}{⟶} ran F \to F^{-1} : ran F \underset{1-1 onto}{⟶} A$
3		f1of1	$⊢ F^{-1} : ran F \underset{1-1 onto}{⟶} A \to F^{-1} : ran F \underset{1-1}{⟶} A$
4		f1veqaeq	$⊢ (F^{-1} : ran F \underset{1-1}{⟶} A \land (C \in ran F \land D \in ran F)) \to (F^{-1} (C) = F^{-1} (D) \to C = D)$
5	4	ex	$⊢ F^{-1} : ran F \underset{1-1}{⟶} A \to ((C \in ran F \land D \in ran F) \to (F^{-1} (C) = F^{-1} (D) \to C = D))$
6	1 2 3 5	4syl	$⊢ F : A \underset{1-1}{⟶} B \to ((C \in ran F \land D \in ran F) \to (F^{-1} (C) = F^{-1} (D) \to C = D))$
7	6	imp	$⊢ (F : A \underset{1-1}{⟶} B \land (C \in ran F \land D \in ran F)) \to (F^{-1} (C) = F^{-1} (D) \to C = D)$