setcepi

Description: An epimorphism of sets is a surjection. (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$
	setcepi.h	$⊢ E = Epi (C)$
	setcepi.2	$⊢ φ \to 2_{𝑜} \in U$
Assertion	setcepi	$⊢ φ \to (F \in (X E Y) \leftrightarrow F : X \underset{onto}{⟶} 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		setcepi.h	$⊢ E = Epi (C)$
6		setcepi.2	$⊢ φ \to 2_{𝑜} \in U$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10	1	setccat	$⊢ U \in V \to C \in Cat$
11	2 10	syl	$⊢ φ \to C \in Cat$
12	1 2	setcbas	$⊢ φ \to U = {Base}_{C}$
13	3 12	eleqtrd	$⊢ φ \to X \in {Base}_{C}$
14	4 12	eleqtrd	$⊢ φ \to Y \in {Base}_{C}$
15	7 8 9 5 11 13 14	epihom	$⊢ φ \to X E Y \subseteq X Hom (C) Y$
16	15	sselda	$⊢ (φ \land F \in (X E Y)) \to F \in (X Hom (C) Y)$
17	1 2 8 3 4	elsetchom	$⊢ φ \to (F \in (X Hom (C) Y) \leftrightarrow F : X ⟶ Y)$
18	17	biimpa	$⊢ (φ \land F \in (X Hom (C) Y)) \to F : X ⟶ Y$
19	16 18	syldan	$⊢ (φ \land F \in (X E Y)) \to F : X ⟶ Y$
20	19	frnd	$⊢ (φ \land F \in (X E Y)) \to ran F \subseteq Y$
21	19	ffnd	$⊢ (φ \land F \in (X E Y)) \to F Fn X$
22		fnfvelrn	$⊢ (F Fn X \land x \in X) \to F (x) \in ran F$
23	21 22	sylan	$⊢ ((φ \land F \in (X E Y)) \land x \in X) \to F (x) \in ran F$
24	23	iftrued	$⊢ ((φ \land F \in (X E Y)) \land x \in X) \to if (F (x) \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜}$
25	24	mpteq2dva	$⊢ (φ \land F \in (X E Y)) \to (x \in X ⟼ if (F (x) \in ran F, 1_{𝑜}, \emptyset)) = (x \in X ⟼ 1_{𝑜})$
26	19	ffvelcdmda	$⊢ ((φ \land F \in (X E Y)) \land x \in X) \to F (x) \in Y$
27	19	feqmptd	$⊢ (φ \land F \in (X E Y)) \to F = (x \in X ⟼ F (x))$
28		eqidd	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) = (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset))$
29		eleq1	$⊢ a = F (x) \to (a \in ran F \leftrightarrow F (x) \in ran F)$
30	29	ifbid	$⊢ a = F (x) \to if (a \in ran F, 1_{𝑜}, \emptyset) = if (F (x) \in ran F, 1_{𝑜}, \emptyset)$
31	26 27 28 30	fmptco	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) \circ F = (x \in X ⟼ if (F (x) \in ran F, 1_{𝑜}, \emptyset))$
32		fconstmpt	$⊢ Y \times \{1_{𝑜}\} = (a \in Y ⟼ 1_{𝑜})$
33	32	a1i	$⊢ (φ \land F \in (X E Y)) \to Y \times \{1_{𝑜}\} = (a \in Y ⟼ 1_{𝑜})$
34		eqidd	$⊢ a = F (x) \to 1_{𝑜} = 1_{𝑜}$
35	26 27 33 34	fmptco	$⊢ (φ \land F \in (X E Y)) \to (Y \times \{1_{𝑜}\}) \circ F = (x \in X ⟼ 1_{𝑜})$
36	25 31 35	3eqtr4d	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) \circ F = (Y \times \{1_{𝑜}\}) \circ F$
37	2	adantr	$⊢ (φ \land F \in (X E Y)) \to U \in V$
38	3	adantr	$⊢ (φ \land F \in (X E Y)) \to X \in U$
39	4	adantr	$⊢ (φ \land F \in (X E Y)) \to Y \in U$
40	6	adantr	$⊢ (φ \land F \in (X E Y)) \to 2_{𝑜} \in U$
41		eqid	$⊢ (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) = (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset))$
42		1oelpr	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
43		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
44	42 43	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
45		0ex	$⊢ \emptyset \in V$
46	45	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
47	46 43	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
48	44 47	ifcli	$⊢ if (a \in ran F, 1_{𝑜}, \emptyset) \in 2_{𝑜}$
49	48	a1i	$⊢ a \in Y \to if (a \in ran F, 1_{𝑜}, \emptyset) \in 2_{𝑜}$
50	41 49	fmpti	$⊢ (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) : Y ⟶ 2_{𝑜}$
51	50	a1i	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) : Y ⟶ 2_{𝑜}$
52	1 37 9 38 39 40 19 51	setcco	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) (⟨X, Y⟩ comp (C) 2_{𝑜}) F = (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) \circ F$
53		fconst6g	$⊢ 1_{𝑜} \in 2_{𝑜} \to (Y \times \{1_{𝑜}\}) : Y ⟶ 2_{𝑜}$
54	44 53	mp1i	$⊢ (φ \land F \in (X E Y)) \to (Y \times \{1_{𝑜}\}) : Y ⟶ 2_{𝑜}$
55	1 37 9 38 39 40 19 54	setcco	$⊢ (φ \land F \in (X E Y)) \to (Y \times \{1_{𝑜}\}) (⟨X, Y⟩ comp (C) 2_{𝑜}) F = (Y \times \{1_{𝑜}\}) \circ F$
56	36 52 55	3eqtr4d	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) (⟨X, Y⟩ comp (C) 2_{𝑜}) F = (Y \times \{1_{𝑜}\}) (⟨X, Y⟩ comp (C) 2_{𝑜}) F$
57	11	adantr	$⊢ (φ \land F \in (X E Y)) \to C \in Cat$
58	13	adantr	$⊢ (φ \land F \in (X E Y)) \to X \in {Base}_{C}$
59	14	adantr	$⊢ (φ \land F \in (X E Y)) \to Y \in {Base}_{C}$
60	6 12	eleqtrd	$⊢ φ \to 2_{𝑜} \in {Base}_{C}$
61	60	adantr	$⊢ (φ \land F \in (X E Y)) \to 2_{𝑜} \in {Base}_{C}$
62		simpr	$⊢ (φ \land F \in (X E Y)) \to F \in (X E Y)$
63	1 37 8 39 40	elsetchom	$⊢ (φ \land F \in (X E Y)) \to ((a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) \in (Y Hom (C) 2_{𝑜}) \leftrightarrow (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) : Y ⟶ 2_{𝑜})$
64	51 63	mpbird	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) \in (Y Hom (C) 2_{𝑜})$
65	1 37 8 39 40	elsetchom	$⊢ (φ \land F \in (X E Y)) \to (Y \times \{1_{𝑜}\} \in (Y Hom (C) 2_{𝑜}) \leftrightarrow (Y \times \{1_{𝑜}\}) : Y ⟶ 2_{𝑜})$
66	54 65	mpbird	$⊢ (φ \land F \in (X E Y)) \to Y \times \{1_{𝑜}\} \in (Y Hom (C) 2_{𝑜})$
67	7 8 9 5 57 58 59 61 62 64 66	epii	$⊢ (φ \land F \in (X E Y)) \to ((a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) (⟨X, Y⟩ comp (C) 2_{𝑜}) F = (Y \times \{1_{𝑜}\}) (⟨X, Y⟩ comp (C) 2_{𝑜}) F \leftrightarrow (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) = Y \times \{1_{𝑜}\})$
68	56 67	mpbid	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) = Y \times \{1_{𝑜}\}$
69	68 32	eqtrdi	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) = (a \in Y ⟼ 1_{𝑜})$
70	48	rgenw	$⊢ \forall a \in Y if (a \in ran F, 1_{𝑜}, \emptyset) \in 2_{𝑜}$
71		mpteqb	$⊢ \forall a \in Y if (a \in ran F, 1_{𝑜}, \emptyset) \in 2_{𝑜} \to ((a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) = (a \in Y ⟼ 1_{𝑜}) \leftrightarrow \forall a \in Y if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜})$
72	70 71	ax-mp	$⊢ (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) = (a \in Y ⟼ 1_{𝑜}) \leftrightarrow \forall a \in Y if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜}$
73	69 72	sylib	$⊢ (φ \land F \in (X E Y)) \to \forall a \in Y if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜}$
74		1n0	$⊢ 1_{𝑜} \neq \emptyset$
75	74	nesymi	$⊢ \neg \emptyset = 1_{𝑜}$
76		iffalse	$⊢ \neg a \in ran F \to if (a \in ran F, 1_{𝑜}, \emptyset) = \emptyset$
77	76	eqeq1d	$⊢ \neg a \in ran F \to (if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜} \leftrightarrow \emptyset = 1_{𝑜})$
78	75 77	mtbiri	$⊢ \neg a \in ran F \to \neg if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜}$
79	78	con4i	$⊢ if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜} \to a \in ran F$
80	79	ralimi	$⊢ \forall a \in Y if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜} \to \forall a \in Y a \in ran F$
81	73 80	syl	$⊢ (φ \land F \in (X E Y)) \to \forall a \in Y a \in ran F$
82		dfss3	$⊢ Y \subseteq ran F \leftrightarrow \forall a \in Y a \in ran F$
83	81 82	sylibr	$⊢ (φ \land F \in (X E Y)) \to Y \subseteq ran F$
84	20 83	eqssd	$⊢ (φ \land F \in (X E Y)) \to ran F = Y$
85		dffo2	$⊢ F : X \underset{onto}{⟶} Y \leftrightarrow (F : X ⟶ Y \land ran F = Y)$
86	19 84 85	sylanbrc	$⊢ (φ \land F \in (X E Y)) \to F : X \underset{onto}{⟶} Y$
87		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
88	87	adantl	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to F : X ⟶ Y$
89	17	biimpar	$⊢ (φ \land F : X ⟶ Y) \to F \in (X Hom (C) Y)$
90	88 89	syldan	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to F \in (X Hom (C) Y)$
91	12	adantr	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to U = {Base}_{C}$
92	91	eleq2d	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to (z \in U \leftrightarrow z \in {Base}_{C})$
93	2	ad2antrr	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to U \in V$
94	3	ad2antrr	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to X \in U$
95	4	ad2antrr	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to Y \in U$
96		simprl	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to z \in U$
97	88	adantr	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to F : X ⟶ Y$
98		simprrl	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to g \in (Y Hom (C) z)$
99	1 93 8 95 96	elsetchom	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to (g \in (Y Hom (C) z) \leftrightarrow g : Y ⟶ z)$
100	98 99	mpbid	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to g : Y ⟶ z$
101	1 93 9 94 95 96 97 100	setcco	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to g (⟨X, Y⟩ comp (C) z) F = g \circ F$
102		simprrr	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to h \in (Y Hom (C) z)$
103	1 93 8 95 96	elsetchom	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to (h \in (Y Hom (C) z) \leftrightarrow h : Y ⟶ z)$
104	102 103	mpbid	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to h : Y ⟶ z$
105	1 93 9 94 95 96 97 104	setcco	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to h (⟨X, Y⟩ comp (C) z) F = h \circ F$
106	101 105	eqeq12d	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to (g (⟨X, Y⟩ comp (C) z) F = h (⟨X, Y⟩ comp (C) z) F \leftrightarrow g \circ F = h \circ F)$
107		simplr	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to F : X \underset{onto}{⟶} Y$
108	100	ffnd	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to g Fn Y$
109	104	ffnd	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to h Fn Y$
110		cocan2	$⊢ (F : X \underset{onto}{⟶} Y \land g Fn Y \land h Fn Y) \to (g \circ F = h \circ F \leftrightarrow g = h)$
111	107 108 109 110	syl3anc	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to (g \circ F = h \circ F \leftrightarrow g = h)$
112	111	biimpd	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to (g \circ F = h \circ F \to g = h)$
113	106 112	sylbid	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land (z \in U \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z)))) \to (g (⟨X, Y⟩ comp (C) z) F = h (⟨X, Y⟩ comp (C) z) F \to g = h)$
114	113	anassrs	$⊢ (((φ \land F : X \underset{onto}{⟶} Y) \land z \in U) \land (g \in (Y Hom (C) z) \land h \in (Y Hom (C) z))) \to (g (⟨X, Y⟩ comp (C) z) F = h (⟨X, Y⟩ comp (C) z) F \to g = h)$
115	114	ralrimivva	$⊢ ((φ \land F : X \underset{onto}{⟶} Y) \land z \in U) \to \forall g \in (Y Hom (C) z) \forall h \in (Y Hom (C) z) (g (⟨X, Y⟩ comp (C) z) F = h (⟨X, Y⟩ comp (C) z) F \to g = h)$
116	115	ex	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to (z \in U \to \forall g \in (Y Hom (C) z) \forall h \in (Y Hom (C) z) (g (⟨X, Y⟩ comp (C) z) F = h (⟨X, Y⟩ comp (C) z) F \to g = h))$
117	92 116	sylbird	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to (z \in {Base}_{C} \to \forall g \in (Y Hom (C) z) \forall h \in (Y Hom (C) z) (g (⟨X, Y⟩ comp (C) z) F = h (⟨X, Y⟩ comp (C) z) F \to g = h))$
118	117	ralrimiv	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to \forall z \in {Base}_{C} \forall g \in (Y Hom (C) z) \forall h \in (Y Hom (C) z) (g (⟨X, Y⟩ comp (C) z) F = h (⟨X, Y⟩ comp (C) z) F \to g = h)$
119	7 8 9 5 11 13 14	isepi2	$⊢ φ \to (F \in (X E Y) \leftrightarrow (F \in (X Hom (C) Y) \land \forall z \in {Base}_{C} \forall g \in (Y Hom (C) z) \forall h \in (Y Hom (C) z) (g (⟨X, Y⟩ comp (C) z) F = h (⟨X, Y⟩ comp (C) z) F \to g = h)))$
120	119	adantr	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to (F \in (X E Y) \leftrightarrow (F \in (X Hom (C) Y) \land \forall z \in {Base}_{C} \forall g \in (Y Hom (C) z) \forall h \in (Y Hom (C) z) (g (⟨X, Y⟩ comp (C) z) F = h (⟨X, Y⟩ comp (C) z) F \to g = h)))$
121	90 118 120	mpbir2and	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to F \in (X E Y)$
122	86 121	impbida	$⊢ φ \to (F \in (X E Y) \leftrightarrow F : X \underset{onto}{⟶} Y)$

Metamath Proof Explorer

Theorem setcepi

Proof