This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to F : A ⟶ B$
		fcof1od.g	$⊢ φ \to G : B ⟶ A$
		fcof1od.a	$⊢ φ \to G \circ F = {I ↾}_{A}$
		fcof1od.b	$⊢ φ \to F \circ G = {I ↾}_{B}$
	Assertion	fcof1od	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		fcof1od.f	$⊢ φ \to F : A ⟶ B$
2		fcof1od.g	$⊢ φ \to G : B ⟶ A$
3		fcof1od.a	$⊢ φ \to G \circ F = {I ↾}_{A}$
4		fcof1od.b	$⊢ φ \to F \circ G = {I ↾}_{B}$
5		fcof1	$⊢ (F : A ⟶ B \land G \circ F = {I ↾}_{A}) \to F : A \underset{1-1}{⟶} B$
6	1 3 5	syl2anc	$⊢ φ \to F : A \underset{1-1}{⟶} B$
7		fcofo	$⊢ (F : A ⟶ B \land G : B ⟶ A \land F \circ G = {I ↾}_{B}) \to F : A \underset{onto}{⟶} B$
8	1 2 4 7	syl3anc	$⊢ φ \to F : A \underset{onto}{⟶} B$
9		df-f1o	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B)$
10	6 8 9	sylanbrc	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$