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

Metamath Proof Explorer

Theorem f1ocnvdm

Description: The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006)

		Ref	Expression
	Assertion	f1ocnvdm	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B) \to F^{-1} (C) \in A$

Step	Hyp	Ref	Expression
1		f1ocnv	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B \underset{1-1 onto}{⟶} A$
2		f1of	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} A \to F^{-1} : B ⟶ A$
3	1 2	syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B ⟶ A$
4	3	ffvelcdmda	$⊢ (F : A \underset{1-1 onto}{⟶} B \land C \in B) \to F^{-1} (C) \in A$