Theorem f1ocnvfvb

Description: Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by NM, 20-May-2004)

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

Proof

Step	Hyp	Ref	Expression
1		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)$$
2	1	3adant3	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(F\left(C\right)=D\to F^{-1}\left(D\right)=C\right)$$
3		fveq2	$$⊢C=F^{-1}\left(D\right)\to F\left(C\right)=F\left(F^{-1}\left(D\right)\right)$$
4	3	eqcoms	$$⊢F^{-1}\left(D\right)=C\to F\left(C\right)=F\left(F^{-1}\left(D\right)\right)$$
5		f1ocnvfv2	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge D\in B\right)\to F\left(F^{-1}\left(D\right)\right)=D$$
6	5	eqeq2d	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge D\in B\right)\to \left(F\left(C\right)=F\left(F^{-1}\left(D\right)\right)\leftrightarrow F\left(C\right)=D\right)$$
7	4 6	imbitrid	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge D\in B\right)\to \left(F^{-1}\left(D\right)=C\to F\left(C\right)=D\right)$$
8	7	3adant2	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(F^{-1}\left(D\right)=C\to F\left(C\right)=D\right)$$
9	2 8	impbid	$$⊢\left(F:A\underset{1-1\; onto}{⟶}B\wedge C\in A\wedge D\in B\right)\to \left(F\left(C\right)=D\leftrightarrow F^{-1}\left(D\right)=C\right)$$