fcof1

Description: An application is injective if a retraction exists. Proposition 8 of BourbakiEns p. E.II.18. (Contributed by FL, 11-Nov-2011) (Revised by Mario Carneiro, 27-Dec-2014)

		Ref	Expression
	Assertion	fcof1	$⊢ (F : A ⟶ B \land R \circ F = {I ↾}_{A}) \to F : A \underset{1-1}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (F : A ⟶ B \land R \circ F = {I ↾}_{A}) \to F : A ⟶ B$
2		simprr	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to F (x) = F (y)$
3	2	fveq2d	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to R (F (x)) = R (F (y))$
4		simpll	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to F : A ⟶ B$
5		simprll	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to x \in A$
6		fvco3	$⊢ (F : A ⟶ B \land x \in A) \to (R \circ F) (x) = R (F (x))$
7	4 5 6	syl2anc	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to (R \circ F) (x) = R (F (x))$
8		simprlr	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to y \in A$
9		fvco3	$⊢ (F : A ⟶ B \land y \in A) \to (R \circ F) (y) = R (F (y))$
10	4 8 9	syl2anc	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to (R \circ F) (y) = R (F (y))$
11	3 7 10	3eqtr4d	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to (R \circ F) (x) = (R \circ F) (y)$
12		simplr	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to R \circ F = {I ↾}_{A}$
13	12	fveq1d	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to (R \circ F) (x) = ({I ↾}_{A}) (x)$
14	12	fveq1d	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to (R \circ F) (y) = ({I ↾}_{A}) (y)$
15	11 13 14	3eqtr3d	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to ({I ↾}_{A}) (x) = ({I ↾}_{A}) (y)$
16		fvresi	$⊢ x \in A \to ({I ↾}_{A}) (x) = x$
17	5 16	syl	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to ({I ↾}_{A}) (x) = x$
18		fvresi	$⊢ y \in A \to ({I ↾}_{A}) (y) = y$
19	8 18	syl	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to ({I ↾}_{A}) (y) = y$
20	15 17 19	3eqtr3d	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land ((x \in A \land y \in A) \land F (x) = F (y))) \to x = y$
21	20	expr	$⊢ ((F : A ⟶ B \land R \circ F = {I ↾}_{A}) \land (x \in A \land y \in A)) \to (F (x) = F (y) \to x = y)$
22	21	ralrimivva	$⊢ (F : A ⟶ B \land R \circ F = {I ↾}_{A}) \to \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)$
23		dff13	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
24	1 22 23	sylanbrc	$⊢ (F : A ⟶ B \land R \circ F = {I ↾}_{A}) \to F : A \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem fcof1

Proof