setcmon

Description: A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	setcmon.c	$⊢ C = SetCat (U)$
	setcmon.u	$⊢ φ \to U \in V$
	setcmon.x	$⊢ φ \to X \in U$
	setcmon.y	$⊢ φ \to Y \in U$
	setcmon.h	$⊢ M = Mono (C)$
Assertion	setcmon	$⊢ φ \to (F \in (X M Y) \leftrightarrow F : X \underset{1-1}{⟶} Y)$

Proof

Step	Hyp	Ref	Expression
1		setcmon.c	$⊢ C = SetCat (U)$
2		setcmon.u	$⊢ φ \to U \in V$
3		setcmon.x	$⊢ φ \to X \in U$
4		setcmon.y	$⊢ φ \to Y \in U$
5		setcmon.h	$⊢ M = Mono (C)$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7		eqid	$⊢ Hom (C) = Hom (C)$
8		eqid	$⊢ comp (C) = comp (C)$
9	1	setccat	$⊢ U \in V \to C \in Cat$
10	2 9	syl	$⊢ φ \to C \in Cat$
11	1 2	setcbas	$⊢ φ \to U = {Base}_{C}$
12	3 11	eleqtrd	$⊢ φ \to X \in {Base}_{C}$
13	4 11	eleqtrd	$⊢ φ \to Y \in {Base}_{C}$
14	6 7 8 5 10 12 13	monhom	$⊢ φ \to X M Y \subseteq X Hom (C) Y$
15	14	sselda	$⊢ (φ \land F \in (X M Y)) \to F \in (X Hom (C) Y)$
16	1 2 7 3 4	elsetchom	$⊢ φ \to (F \in (X Hom (C) Y) \leftrightarrow F : X ⟶ Y)$
17	16	biimpa	$⊢ (φ \land F \in (X Hom (C) Y)) \to F : X ⟶ Y$
18	15 17	syldan	$⊢ (φ \land F \in (X M Y)) \to F : X ⟶ Y$
19		simprr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F (x) = F (y)$
20	19	sneqd	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to \{F (x)\} = \{F (y)\}$
21	20	xpeq2d	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to X \times \{F (x)\} = X \times \{F (y)\}$
22	18	adantr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F : X ⟶ Y$
23	22	ffnd	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F Fn X$
24		simprll	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to x \in X$
25		fcoconst	$⊢ (F Fn X \land x \in X) \to F \circ (X \times \{x\}) = X \times \{F (x)\}$
26	23 24 25	syl2anc	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F \circ (X \times \{x\}) = X \times \{F (x)\}$
27		simprlr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to y \in X$
28		fcoconst	$⊢ (F Fn X \land y \in X) \to F \circ (X \times \{y\}) = X \times \{F (y)\}$
29	23 27 28	syl2anc	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F \circ (X \times \{y\}) = X \times \{F (y)\}$
30	21 26 29	3eqtr4d	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F \circ (X \times \{x\}) = F \circ (X \times \{y\})$
31	2	ad2antrr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to U \in V$
32	3	ad2antrr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to X \in U$
33	4	ad2antrr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to Y \in U$
34		fconst6g	$⊢ x \in X \to (X \times \{x\}) : X ⟶ X$
35	24 34	syl	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to (X \times \{x\}) : X ⟶ X$
36	1 31 8 32 32 33 35 22	setcco	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F (⟨X, X⟩ comp (C) Y) (X \times \{x\}) = F \circ (X \times \{x\})$
37		fconst6g	$⊢ y \in X \to (X \times \{y\}) : X ⟶ X$
38	27 37	syl	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to (X \times \{y\}) : X ⟶ X$
39	1 31 8 32 32 33 38 22	setcco	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F (⟨X, X⟩ comp (C) Y) (X \times \{y\}) = F \circ (X \times \{y\})$
40	30 36 39	3eqtr4d	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F (⟨X, X⟩ comp (C) Y) (X \times \{x\}) = F (⟨X, X⟩ comp (C) Y) (X \times \{y\})$
41	10	ad2antrr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to C \in Cat$
42	12	ad2antrr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to X \in {Base}_{C}$
43	13	ad2antrr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to Y \in {Base}_{C}$
44		simplr	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to F \in (X M Y)$
45	1 31 7 32 32	elsetchom	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to (X \times \{x\} \in (X Hom (C) X) \leftrightarrow (X \times \{x\}) : X ⟶ X)$
46	35 45	mpbird	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to X \times \{x\} \in (X Hom (C) X)$
47	1 31 7 32 32	elsetchom	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to (X \times \{y\} \in (X Hom (C) X) \leftrightarrow (X \times \{y\}) : X ⟶ X)$
48	38 47	mpbird	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to X \times \{y\} \in (X Hom (C) X)$
49	6 7 8 5 41 42 43 42 44 46 48	moni	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to (F (⟨X, X⟩ comp (C) Y) (X \times \{x\}) = F (⟨X, X⟩ comp (C) Y) (X \times \{y\}) \leftrightarrow X \times \{x\} = X \times \{y\})$
50	40 49	mpbid	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to X \times \{x\} = X \times \{y\}$
51	50	fveq1d	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to (X \times \{x\}) (x) = (X \times \{y\}) (x)$
52		vex	$⊢ x \in V$
53	52	fvconst2	$⊢ x \in X \to (X \times \{x\}) (x) = x$
54	24 53	syl	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to (X \times \{x\}) (x) = x$
55		vex	$⊢ y \in V$
56	55	fvconst2	$⊢ x \in X \to (X \times \{y\}) (x) = y$
57	24 56	syl	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to (X \times \{y\}) (x) = y$
58	51 54 57	3eqtr3d	$⊢ ((φ \land F \in (X M Y)) \land ((x \in X \land y \in X) \land F (x) = F (y))) \to x = y$
59	58	expr	$⊢ ((φ \land F \in (X M Y)) \land (x \in X \land y \in X)) \to (F (x) = F (y) \to x = y)$
60	59	ralrimivva	$⊢ (φ \land F \in (X M Y)) \to \forall x \in X \forall y \in X (F (x) = F (y) \to x = y)$
61		dff13	$⊢ F : X \underset{1-1}{⟶} Y \leftrightarrow (F : X ⟶ Y \land \forall x \in X \forall y \in X (F (x) = F (y) \to x = y))$
62	18 60 61	sylanbrc	$⊢ (φ \land F \in (X M Y)) \to F : X \underset{1-1}{⟶} Y$
63		f1f	$⊢ F : X \underset{1-1}{⟶} Y \to F : X ⟶ Y$
64	16	biimpar	$⊢ (φ \land F : X ⟶ Y) \to F \in (X Hom (C) Y)$
65	63 64	sylan2	$⊢ (φ \land F : X \underset{1-1}{⟶} Y) \to F \in (X Hom (C) Y)$
66	11	adantr	$⊢ (φ \land F : X \underset{1-1}{⟶} Y) \to U = {Base}_{C}$
67	66	eleq2d	$⊢ (φ \land F : X \underset{1-1}{⟶} Y) \to (z \in U \leftrightarrow z \in {Base}_{C})$
68	2	ad2antrr	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to U \in V$
69		simprl	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to z \in U$
70	3	ad2antrr	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to X \in U$
71	4	ad2antrr	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to Y \in U$
72		simprrl	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to g \in (z Hom (C) X)$
73	1 68 7 69 70	elsetchom	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to (g \in (z Hom (C) X) \leftrightarrow g : z ⟶ X)$
74	72 73	mpbid	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to g : z ⟶ X$
75	63	ad2antlr	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to F : X ⟶ Y$
76	1 68 8 69 70 71 74 75	setcco	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to F (⟨z, X⟩ comp (C) Y) g = F \circ g$
77		simprrr	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to h \in (z Hom (C) X)$
78	1 68 7 69 70	elsetchom	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to (h \in (z Hom (C) X) \leftrightarrow h : z ⟶ X)$
79	77 78	mpbid	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to h : z ⟶ X$
80	1 68 8 69 70 71 79 75	setcco	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to F (⟨z, X⟩ comp (C) Y) h = F \circ h$
81	76 80	eqeq12d	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to (F (⟨z, X⟩ comp (C) Y) g = F (⟨z, X⟩ comp (C) Y) h \leftrightarrow F \circ g = F \circ h)$
82		simplr	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to F : X \underset{1-1}{⟶} Y$
83		cocan1	$⊢ (F : X \underset{1-1}{⟶} Y \land g : z ⟶ X \land h : z ⟶ X) \to (F \circ g = F \circ h \leftrightarrow g = h)$
84	82 74 79 83	syl3anc	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to (F \circ g = F \circ h \leftrightarrow g = h)$
85	84	biimpd	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to (F \circ g = F \circ h \to g = h)$
86	81 85	sylbid	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land (z \in U \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X)))) \to (F (⟨z, X⟩ comp (C) Y) g = F (⟨z, X⟩ comp (C) Y) h \to g = h)$
87	86	anassrs	$⊢ (((φ \land F : X \underset{1-1}{⟶} Y) \land z \in U) \land (g \in (z Hom (C) X) \land h \in (z Hom (C) X))) \to (F (⟨z, X⟩ comp (C) Y) g = F (⟨z, X⟩ comp (C) Y) h \to g = h)$
88	87	ralrimivva	$⊢ ((φ \land F : X \underset{1-1}{⟶} Y) \land z \in U) \to \forall g \in (z Hom (C) X) \forall h \in (z Hom (C) X) (F (⟨z, X⟩ comp (C) Y) g = F (⟨z, X⟩ comp (C) Y) h \to g = h)$
89	88	ex	$⊢ (φ \land F : X \underset{1-1}{⟶} Y) \to (z \in U \to \forall g \in (z Hom (C) X) \forall h \in (z Hom (C) X) (F (⟨z, X⟩ comp (C) Y) g = F (⟨z, X⟩ comp (C) Y) h \to g = h))$
90	67 89	sylbird	$⊢ (φ \land F : X \underset{1-1}{⟶} Y) \to (z \in {Base}_{C} \to \forall g \in (z Hom (C) X) \forall h \in (z Hom (C) X) (F (⟨z, X⟩ comp (C) Y) g = F (⟨z, X⟩ comp (C) Y) h \to g = h))$
91	90	ralrimiv	$⊢ (φ \land F : X \underset{1-1}{⟶} Y) \to \forall z \in {Base}_{C} \forall g \in (z Hom (C) X) \forall h \in (z Hom (C) X) (F (⟨z, X⟩ comp (C) Y) g = F (⟨z, X⟩ comp (C) Y) h \to g = h)$
92	6 7 8 5 10 12 13	ismon2	$⊢ φ \to (F \in (X M Y) \leftrightarrow (F \in (X Hom (C) Y) \land \forall z \in {Base}_{C} \forall g \in (z Hom (C) X) \forall h \in (z Hom (C) X) (F (⟨z, X⟩ comp (C) Y) g = F (⟨z, X⟩ comp (C) Y) h \to g = h)))$
93	92	adantr	$⊢ (φ \land F : X \underset{1-1}{⟶} Y) \to (F \in (X M Y) \leftrightarrow (F \in (X Hom (C) Y) \land \forall z \in {Base}_{C} \forall g \in (z Hom (C) X) \forall h \in (z Hom (C) X) (F (⟨z, X⟩ comp (C) Y) g = F (⟨z, X⟩ comp (C) Y) h \to g = h)))$
94	65 91 93	mpbir2and	$⊢ (φ \land F : X \underset{1-1}{⟶} Y) \to F \in (X M Y)$
95	62 94	impbida	$⊢ φ \to (F \in (X M Y) \leftrightarrow F : X \underset{1-1}{⟶} Y)$

Metamath Proof Explorer

Theorem setcmon

Proof