Theorem fcof1od

Description: A function is bijective if a "retraction" and a "section" exist, see comments for fcof1 and fcofo . Formerly part of proof of fcof1o . (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	fcof1od.f	$$⊢\phi \to F:A⟶B$$
	fcof1od.g	$$⊢\phi \to G:B⟶A$$
	fcof1od.a	$$⊢\phi \to G\circ F={\mathrm{I}\upharpoonright }_A$$
	fcof1od.b	$$⊢\phi \to F\circ G={\mathrm{I}\upharpoonright }_B$$
Assertion	fcof1od	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		fcof1od.f	$$⊢\phi \to F:A⟶B$$
2		fcof1od.g	$$⊢\phi \to G:B⟶A$$
3		fcof1od.a	$$⊢\phi \to G\circ F={\mathrm{I}\upharpoonright }_A$$
4		fcof1od.b	$$⊢\phi \to F\circ G={\mathrm{I}\upharpoonright }_B$$
5		fcof1	$$⊢\left(F:A⟶B\wedge G\circ F={\mathrm{I}\upharpoonright }_A\right)\to F:A\underset{1-1}{⟶}B$$
6	1 3 5	syl2anc	$$⊢\phi \to F:A\underset{1-1}{⟶}B$$
7		fcofo	$$⊢\left(F:A⟶B\wedge G:B⟶A\wedge F\circ G={\mathrm{I}\upharpoonright }_B\right)\to F:A\underset{onto}{⟶}B$$
8	1 2 4 7	syl3anc	$$⊢\phi \to F:A\underset{onto}{⟶}B$$
9		df-f1o	$$⊢F:A\underset{1-1\; onto}{⟶}B\leftrightarrow \left(F:A\underset{1-1}{⟶}B\wedge F:A\underset{onto}{⟶}B\right)$$
10	6 8 9	sylanbrc	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$