Theorem f1o2d

Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014)

	Ref	Expression
Hypotheses	f1od.1	$$⊢F=\left(x\in A⟼C\right)$$
	f1o2d.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
	f1o2d.3	$$⊢\left(\phi \wedge y\in B\right)\to D\in A$$
	f1o2d.4	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to \left(x=D\leftrightarrow y=C\right)$$
Assertion	f1o2d	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		f1od.1	$$⊢F=\left(x\in A⟼C\right)$$
2		f1o2d.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in B$$
3		f1o2d.3	$$⊢\left(\phi \wedge y\in B\right)\to D\in A$$
4		f1o2d.4	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to \left(x=D\leftrightarrow y=C\right)$$
5	1 2 3 4	f1ocnv2d	$$⊢\phi \to \left(F:A\underset{1-1\; onto}{⟶}B\wedge F^{-1}=\left(y\in B⟼D\right)\right)$$
6	5	simpld	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$