Theorem f1od

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)$$
	f1od.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in W$$
	f1od.3	$$⊢\left(\phi \wedge y\in B\right)\to D\in X$$
	f1od.4	$$⊢\phi \to \left(\left(x\in A\wedge y=C\right)\leftrightarrow \left(y\in B\wedge x=D\right)\right)$$
Assertion	f1od	$$⊢\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		f1od.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in W$$
3		f1od.3	$$⊢\left(\phi \wedge y\in B\right)\to D\in X$$
4		f1od.4	$$⊢\phi \to \left(\left(x\in A\wedge y=C\right)\leftrightarrow \left(y\in B\wedge x=D\right)\right)$$
5	1 2 3 4	f1ocnvd	$$⊢\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$$