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	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in B\right)\to F^{-1}\left(C\right)\in A$$

Proof

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	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in B\right)\to F^{-1}\left(C\right)\in A$$