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	ffvelrnda	$⊢ ((φ \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		1oex	$⊢ 1_{𝑜} \in V$
43	42	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
44		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
45	43 44	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
46		0ex	$⊢ \emptyset \in V$
47	46	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
48	47 44	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
49	45 48	ifcli	$⊢ if (a \in ran F, 1_{𝑜}, \emptyset) \in 2_{𝑜}$
50	49	a1i	$⊢ a \in Y \to if (a \in ran F, 1_{𝑜}, \emptyset) \in 2_{𝑜}$
51	41 50	fmpti	$⊢ (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) : Y ⟶ 2_{𝑜}$
52	51	a1i	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) : Y ⟶ 2_{𝑜}$
53	1 37 9 38 39 40 19 52	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$
54		fconst6g	$⊢ 1_{𝑜} \in 2_{𝑜} \to (Y \times \{1_{𝑜}\}) : Y ⟶ 2_{𝑜}$
55	45 54	mp1i	$⊢ (φ \land F \in (X E Y)) \to (Y \times \{1_{𝑜}\}) : Y ⟶ 2_{𝑜}$
56	1 37 9 38 39 40 19 55	setcco	$⊢ (φ \land F \in (X E Y)) \to (Y \times \{1_{𝑜}\}) (⟨X, Y⟩ comp (C) 2_{𝑜}) F = (Y \times \{1_{𝑜}\}) \circ F$
57	36 53 56	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$
58	11	adantr	$⊢ (φ \land F \in (X E Y)) \to C \in Cat$
59	13	adantr	$⊢ (φ \land F \in (X E Y)) \to X \in {Base}_{C}$
60	14	adantr	$⊢ (φ \land F \in (X E Y)) \to Y \in {Base}_{C}$
61	6 12	eleqtrd	$⊢ φ \to 2_{𝑜} \in {Base}_{C}$
62	61	adantr	$⊢ (φ \land F \in (X E Y)) \to 2_{𝑜} \in {Base}_{C}$
63		simpr	$⊢ (φ \land F \in (X E Y)) \to F \in (X E Y)$
64	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_{𝑜})$
65	52 64	mpbird	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) \in (Y Hom (C) 2_{𝑜})$
66	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_{𝑜})$
67	55 66	mpbird	$⊢ (φ \land F \in (X E Y)) \to Y \times \{1_{𝑜}\} \in (Y Hom (C) 2_{𝑜})$
68	7 8 9 5 58 59 60 62 63 65 67	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_{𝑜}\})$
69	57 68	mpbid	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) = Y \times \{1_{𝑜}\}$
70	69 32	eqtrdi	$⊢ (φ \land F \in (X E Y)) \to (a \in Y ⟼ if (a \in ran F, 1_{𝑜}, \emptyset)) = (a \in Y ⟼ 1_{𝑜})$
71	49	rgenw	$⊢ \forall a \in Y if (a \in ran F, 1_{𝑜}, \emptyset) \in 2_{𝑜}$
72		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_{𝑜})$
73	71 72	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_{𝑜}$
74	70 73	sylib	$⊢ (φ \land F \in (X E Y)) \to \forall a \in Y if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜}$
75		1n0	$⊢ 1_{𝑜} \neq \emptyset$
76	75	nesymi	$⊢ \neg \emptyset = 1_{𝑜}$
77		iffalse	$⊢ \neg a \in ran F \to if (a \in ran F, 1_{𝑜}, \emptyset) = \emptyset$
78	77	eqeq1d	$⊢ \neg a \in ran F \to (if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜} \leftrightarrow \emptyset = 1_{𝑜})$
79	76 78	mtbiri	$⊢ \neg a \in ran F \to \neg if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜}$
80	79	con4i	$⊢ if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜} \to a \in ran F$
81	80	ralimi	$⊢ \forall a \in Y if (a \in ran F, 1_{𝑜}, \emptyset) = 1_{𝑜} \to \forall a \in Y a \in ran F$
82	74 81	syl	$⊢ (φ \land F \in (X E Y)) \to \forall a \in Y a \in ran F$
83		dfss3	$⊢ Y \subseteq ran F \leftrightarrow \forall a \in Y a \in ran F$
84	82 83	sylibr	$⊢ (φ \land F \in (X E Y)) \to Y \subseteq ran F$
85	20 84	eqssd	$⊢ (φ \land F \in (X E Y)) \to ran F = Y$
86		dffo2	$⊢ F : X \underset{onto}{⟶} Y \leftrightarrow (F : X ⟶ Y \land ran F = Y)$
87	19 85 86	sylanbrc	$⊢ (φ \land F \in (X E Y)) \to F : X \underset{onto}{⟶} Y$
88		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
89	88	adantl	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to F : X ⟶ Y$
90	17	biimpar	$⊢ (φ \land F : X ⟶ Y) \to F \in (X Hom (C) Y)$
91	89 90	syldan	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to F \in (X Hom (C) Y)$
92	12	adantr	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to U = {Base}_{C}$
93	92	eleq2d	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to (z \in U \leftrightarrow z \in {Base}_{C})$
94	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$
95	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$
96	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$
97		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$
98	89	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$
99		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)$
100	1 94 8 96 97	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)$
101	99 100	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$
102	1 94 9 95 96 97 98 101	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$
103		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)$
104	1 94 8 96 97	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)$
105	103 104	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$
106	1 94 9 95 96 97 98 105	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$
107	102 106	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)$
108		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$
109	101	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$
110	105	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$
111		cocan2	$⊢ (F : X \underset{onto}{⟶} Y \land g Fn Y \land h Fn Y) \to (g \circ F = h \circ F \leftrightarrow g = h)$
112	108 109 110 111	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)$
113	112	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)$
114	107 113	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)$
115	114	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)$
116	115	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)$
117	116	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))$
118	93 117	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))$
119	118	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)$
120	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)))$
121	120	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)))$
122	91 119 121	mpbir2and	$⊢ (φ \land F : X \underset{onto}{⟶} Y) \to F \in (X E Y)$
123	87 122	impbida	$⊢ φ \to (F \in (X E Y) \leftrightarrow F : X \underset{onto}{⟶} Y)$

Metamath Proof Explorer

Theorem setcepi

Proof