Theorem f1ocnvfv

Description: Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004)

	Ref	Expression
Assertion	f1ocnvfv	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\right)\to \left(F\left(C\right)=D\to F^{-1}\left(D\right)=C\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢D=F\left(C\right)\to F^{-1}\left(D\right)=F^{-1}\left(F\left(C\right)\right)$$
2	1	eqcoms	$$⊢F\left(C\right)=D\to F^{-1}\left(D\right)=F^{-1}\left(F\left(C\right)\right)$$
3		f1ocnvfv1	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\right)\to F^{-1}\left(F\left(C\right)\right)=C$$
4	3	eqeq2d	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\right)\to \left(F^{-1}\left(D\right)=F^{-1}\left(F\left(C\right)\right)\leftrightarrow F^{-1}\left(D\right)=C\right)$$
5	2 4	imbitrid	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\right)\to \left(F\left(C\right)=D\to F^{-1}\left(D\right)=C\right)$$