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

Metamath Proof Explorer

Theorem fcofo

Description: An application is surjective if a section exists. Proposition 8 of BourbakiEns p. E.II.18. (Contributed by FL, 17-Nov-2011) (Proof shortened by Mario Carneiro, 27-Dec-2014)

		Ref	Expression
	Assertion	fcofo	$⊢ (F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \to F : A \underset{onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \to F : A ⟶ B$
2		ffvelcdm	$⊢ (S : B ⟶ A \land y \in B) \to S (y) \in A$
3	2	3ad2antl2	$⊢ ((F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \land y \in B) \to S (y) \in A$
4		simpl3	$⊢ ((F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \land y \in B) \to F \circ S = {I ↾}_{B}$
5	4	fveq1d	$⊢ ((F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \land y \in B) \to (F \circ S) (y) = ({I ↾}_{B}) (y)$
6		fvco3	$⊢ (S : B ⟶ A \land y \in B) \to (F \circ S) (y) = F (S (y))$
7	6	3ad2antl2	$⊢ ((F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \land y \in B) \to (F \circ S) (y) = F (S (y))$
8		fvresi	$⊢ y \in B \to ({I ↾}_{B}) (y) = y$
9	8	adantl	$⊢ ((F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \land y \in B) \to ({I ↾}_{B}) (y) = y$
10	5 7 9	3eqtr3rd	$⊢ ((F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \land y \in B) \to y = F (S (y))$
11		fveq2	$⊢ x = S (y) \to F (x) = F (S (y))$
12	11	rspceeqv	$⊢ (S (y) \in A \land y = F (S (y))) \to \exists x \in A y = F (x)$
13	3 10 12	syl2anc	$⊢ ((F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \land y \in B) \to \exists x \in A y = F (x)$
14	13	ralrimiva	$⊢ (F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \to \forall y \in B \exists x \in A y = F (x)$
15		dffo3	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall y \in B \exists x \in A y = F (x))$
16	1 14 15	sylanbrc	$⊢ (F : A ⟶ B \land S : B ⟶ A \land F \circ S = {I ↾}_{B}) \to F : A \underset{onto}{⟶} B$