Theorem setcepi 16738

Description: An epimorphism of sets is a surjection. (Contributed by Mario Carneiro, 3-Jan-2017.)

Hypotheses

Ref	Expression
setcmon.c	⊢ 𝐶 = (SetCat‘𝑈)
setcmon.u	⊢ (𝜑 → 𝑈 ∈ 𝑉)
setcmon.x	⊢ (𝜑 → 𝑋 ∈ 𝑈)
setcmon.y	⊢ (𝜑 → 𝑌 ∈ 𝑈)
setcepi.h	⊢ 𝐸 = (Epi‘𝐶)
setcepi.2	⊢ (𝜑 → 2𝑜 ∈ 𝑈)

Assertion

Ref	Expression
setcepi	⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋–onto→𝑌))

Proof of Theorem setcepi

Dummy variables 𝑥 𝑔 𝑎 ℎ 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . . . . 6 ⊢ (Base‘𝐶) = (Base‘𝐶)
2		eqid 2622	. . . . . 6 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
3		eqid 2622	. . . . . 6 ⊢ (comp‘𝐶) = (comp‘𝐶)
4		setcepi.h	. . . . . 6 ⊢ 𝐸 = (Epi‘𝐶)
5		setcmon.u	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
6		setcmon.c	. . . . . . . 8 ⊢ 𝐶 = (SetCat‘𝑈)
7	6	setccat 16735	. . . . . . 7 ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
8	5, 7	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ Cat)
9		setcmon.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
10	6, 5	setcbas 16728	. . . . . . 7 ⊢ (𝜑 → 𝑈 = (Base‘𝐶))
11	9, 10	eleqtrd 2703	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶))
12		setcmon.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑈)
13	12, 10	eleqtrd 2703	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐶))
14	1, 2, 3, 4, 8, 11, 13	epihom 16402	. . . . 5 ⊢ (𝜑 → (𝑋𝐸𝑌) ⊆ (𝑋(Hom ‘𝐶)𝑌))
15	14	sselda 3603	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
16	6, 5, 2, 9, 12	elsetchom 16731	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ↔ 𝐹:𝑋⟶𝑌))
17	16	biimpa 501	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) → 𝐹:𝑋⟶𝑌)
18	15, 17	syldan 487	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹:𝑋⟶𝑌)
19		frn 6053	. . . . 5 ⊢ (𝐹:𝑋⟶𝑌 → ran 𝐹 ⊆ 𝑌)
20	18, 19	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹 ⊆ 𝑌)
21		ffn 6045	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝑋⟶𝑌 → 𝐹 Fn 𝑋)
22	18, 21	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 Fn 𝑋)
23		fnfvelrn 6356	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ran 𝐹)
24	22, 23	sylan 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ran 𝐹)
25	24	iftrued 4094	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥 ∈ 𝑋) → if((𝐹‘𝑥) ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜)
26	25	mpteq2dva 4744	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑥 ∈ 𝑋 ↦ if((𝐹‘𝑥) ∈ ran 𝐹, 1𝑜, ∅)) = (𝑥 ∈ 𝑋 ↦ 1𝑜))
27	18	ffvelrnda 6359	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ 𝑌)
28	18	feqmptd 6249	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐹‘𝑥)))
29		eqidd 2623	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)))
30		eleq1 2689	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝐹‘𝑥) → (𝑎 ∈ ran 𝐹 ↔ (𝐹‘𝑥) ∈ ran 𝐹))
31	30	ifbid 4108	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝐹‘𝑥) → if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = if((𝐹‘𝑥) ∈ ran 𝐹, 1𝑜, ∅))
32	27, 28, 29, 31	fmptco 6396	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∘ 𝐹) = (𝑥 ∈ 𝑋 ↦ if((𝐹‘𝑥) ∈ ran 𝐹, 1𝑜, ∅)))
33		fconstmpt 5163	. . . . . . . . . . . . 13 ⊢ (𝑌 × {1𝑜}) = (𝑎 ∈ 𝑌 ↦ 1𝑜)
34	33	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1𝑜}) = (𝑎 ∈ 𝑌 ↦ 1𝑜))
35		eqidd 2623	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝐹‘𝑥) → 1𝑜 = 1𝑜)
36	27, 28, 34, 35	fmptco 6396	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1𝑜}) ∘ 𝐹) = (𝑥 ∈ 𝑋 ↦ 1𝑜))
37	26, 32, 36	3eqtr4d 2666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∘ 𝐹) = ((𝑌 × {1𝑜}) ∘ 𝐹))
38	5	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑈 ∈ 𝑉)
39	9	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋 ∈ 𝑈)
40	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ∈ 𝑈)
41		setcepi.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 2𝑜 ∈ 𝑈)
42	41	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 2𝑜 ∈ 𝑈)
43		eqid 2622	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅))
44		1onn 7719	. . . . . . . . . . . . . . . . . 18 ⊢ 1𝑜 ∈ ω
45	44	elexi 3213	. . . . . . . . . . . . . . . . 17 ⊢ 1𝑜 ∈ V
46	45	prid2 4298	. . . . . . . . . . . . . . . 16 ⊢ 1𝑜 ∈ {∅, 1𝑜}
47		df2o3 7573	. . . . . . . . . . . . . . . 16 ⊢ 2𝑜 = {∅, 1𝑜}
48	46, 47	eleqtrri 2700	. . . . . . . . . . . . . . 15 ⊢ 1𝑜 ∈ 2𝑜
49		0ex 4790	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
50	49	prid1 4297	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ {∅, 1𝑜}
51	50, 47	eleqtrri 2700	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ 2𝑜
52	48, 51	keepel 4155	. . . . . . . . . . . . . 14 ⊢ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈ 2𝑜
53	52	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑌 → if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈ 2𝑜)
54	43, 53	fmpti 6383	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)):𝑌⟶2𝑜
55	54	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)):𝑌⟶2𝑜)
56	6, 38, 3, 39, 40, 42, 18, 55	setcco 16733	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅))(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) = ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∘ 𝐹))
57		fconst6g 6094	. . . . . . . . . . . 12 ⊢ (1𝑜 ∈ 2𝑜 → (𝑌 × {1𝑜}):𝑌⟶2𝑜)
58	48, 57	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1𝑜}):𝑌⟶2𝑜)
59	6, 38, 3, 39, 40, 42, 18, 58	setcco 16733	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1𝑜})(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) = ((𝑌 × {1𝑜}) ∘ 𝐹))
60	37, 56, 59	3eqtr4d 2666	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅))(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) = ((𝑌 × {1𝑜})(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹))
61	8	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐶 ∈ Cat)
62	11	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋 ∈ (Base‘𝐶))
63	13	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ∈ (Base‘𝐶))
64	41, 10	eleqtrd 2703	. . . . . . . . . . 11 ⊢ (𝜑 → 2𝑜 ∈ (Base‘𝐶))
65	64	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 2𝑜 ∈ (Base‘𝐶))
66		simpr 477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 ∈ (𝑋𝐸𝑌))
67	6, 38, 2, 40, 42	elsetchom 16731	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∈ (𝑌(Hom ‘𝐶)2𝑜) ↔ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)):𝑌⟶2𝑜))
68	55, 67	mpbird 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∈ (𝑌(Hom ‘𝐶)2𝑜))
69	6, 38, 2, 40, 42	elsetchom 16731	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1𝑜}) ∈ (𝑌(Hom ‘𝐶)2𝑜) ↔ (𝑌 × {1𝑜}):𝑌⟶2𝑜))
70	58, 69	mpbird 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1𝑜}) ∈ (𝑌(Hom ‘𝐶)2𝑜))
71	1, 2, 3, 4, 61, 62, 63, 65, 66, 68, 70	epii 16403	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅))(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) = ((𝑌 × {1𝑜})(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) ↔ (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑌 × {1𝑜})))
72	60, 71	mpbid 222	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑌 × {1𝑜}))
73	72, 33	syl6eq 2672	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦ 1𝑜))
74	52	rgenw 2924	. . . . . . . 8 ⊢ ∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈ 2𝑜
75		mpteqb 6299	. . . . . . . 8 ⊢ (∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈ 2𝑜 → ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦ 1𝑜) ↔ ∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜))
76	74, 75	ax-mp 5	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎 ∈ 𝑌 ↦ 1𝑜) ↔ ∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜)
77	73, 76	sylib 208	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜)
78		1n0 7575	. . . . . . . . . 10 ⊢ 1𝑜 ≠ ∅
79	78	nesymi 2851	. . . . . . . . 9 ⊢ ¬ ∅ = 1𝑜
80		iffalse 4095	. . . . . . . . . 10 ⊢ (¬ 𝑎 ∈ ran 𝐹 → if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = ∅)
81	80	eqeq1d 2624	. . . . . . . . 9 ⊢ (¬ 𝑎 ∈ ran 𝐹 → (if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜 ↔ ∅ = 1𝑜))
82	79, 81	mtbiri 317	. . . . . . . 8 ⊢ (¬ 𝑎 ∈ ran 𝐹 → ¬ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜)
83	82	con4i 113	. . . . . . 7 ⊢ (if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜 → 𝑎 ∈ ran 𝐹)
84	83	ralimi 2952	. . . . . 6 ⊢ (∀𝑎 ∈ 𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜 → ∀𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹)
85	77, 84	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹)
86		dfss3 3592	. . . . 5 ⊢ (𝑌 ⊆ ran 𝐹 ↔ ∀𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹)
87	85, 86	sylibr 224	. . . 4 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ⊆ ran 𝐹)
88	20, 87	eqssd 3620	. . 3 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹 = 𝑌)
89		dffo2 6119	. . 3 ⊢ (𝐹:𝑋–onto→𝑌 ↔ (𝐹:𝑋⟶𝑌 ∧ ran 𝐹 = 𝑌))
90	18, 88, 89	sylanbrc 698	. 2 ⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹:𝑋–onto→𝑌)
91		fof 6115	. . . . 5 ⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌)
92	91	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝐹:𝑋⟶𝑌)
93	16	biimpar 502	. . . 4 ⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
94	92, 93	syldan 487	. . 3 ⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
95	10	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝑈 = (Base‘𝐶))
96	95	eleq2d 2687	. . . . 5 ⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ 𝑈 ↔ 𝑧 ∈ (Base‘𝐶)))
97	5	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑈 ∈ 𝑉)
98	9	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑋 ∈ 𝑈)
99	12	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑌 ∈ 𝑈)
100		simprl 794	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ 𝑈)
101	92	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋⟶𝑌)
102		simprrl 804	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧))
103	6, 97, 2, 99, 100	elsetchom 16731	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ 𝑔:𝑌⟶𝑧))
104	102, 103	mpbid 222	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔:𝑌⟶𝑧)
105	6, 97, 3, 98, 99, 100, 101, 104	setcco 16733	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (𝑔 ∘ 𝐹))
106		simprrr 805	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))
107	6, 97, 2, 99, 100	elsetchom 16731	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (ℎ ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ ℎ:𝑌⟶𝑧))
108	106, 107	mpbid 222	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ℎ:𝑌⟶𝑧)
109	6, 97, 3, 98, 99, 100, 101, 108	setcco 16733	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ ∘ 𝐹))
110	105, 109	eqeq12d 2637	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) ↔ (𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹)))
111		simplr 792	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋–onto→𝑌)
112		ffn 6045	. . . . . . . . . . . 12 ⊢ (𝑔:𝑌⟶𝑧 → 𝑔 Fn 𝑌)
113	104, 112	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 Fn 𝑌)
114		ffn 6045	. . . . . . . . . . . 12 ⊢ (ℎ:𝑌⟶𝑧 → ℎ Fn 𝑌)
115	108, 114	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ℎ Fn 𝑌)
116		cocan2 6547	. . . . . . . . . . 11 ⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑔 Fn 𝑌 ∧ ℎ Fn 𝑌) → ((𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹) ↔ 𝑔 = ℎ))
117	111, 113, 115, 116	syl3anc 1326	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹) ↔ 𝑔 = ℎ))
118	117	biimpd 219	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔 ∘ 𝐹) = (ℎ ∘ 𝐹) → 𝑔 = ℎ))
119	110, 118	sylbid 230	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ (𝑧 ∈ 𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))
120	119	anassrs 680	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝑧 ∈ 𝑈) ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ℎ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))
121	120	ralrimivva 2971	. . . . . 6 ⊢ (((𝜑 ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝑧 ∈ 𝑈) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))
122	121	ex 450	. . . . 5 ⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ 𝑈 → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)))
123	96, 122	sylbird 250	. . . 4 ⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ (Base‘𝐶) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ)))
124	123	ralrimiv 2965	. . 3 ⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))
125	1, 2, 3, 4, 8, 11, 13	isepi2 16401	. . . 4 ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))))
126	125	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (ℎ(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ℎ))))
127	94, 124, 126	mpbir2and 957	. 2 ⊢ ((𝜑 ∧ 𝐹:𝑋–onto→𝑌) → 𝐹 ∈ (𝑋𝐸𝑌))
128	90, 127	impbida 877	1 ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋–onto→𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912   ⊆ wss 3574  ∅c0 3915  ifcif 4086  {csn 4177  {cpr 4179  ⟨cop 4183   ↦ cmpt 4729   × cxp 5112  ran crn 5115   ∘ ccom 5118   Fn wfn 5883  ⟶wf 5884  –onto→wfo 5886  ‘cfv 5888  (class class class)co 6650  ωcom 7065  1_𝑜c1o 7553  2_𝑜c2o 7554  Basecbs 15857  Hom chom 15952  compcco 15953  Catccat 16325  Epicepi 16389  SetCatcsetc 16725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-fz 12327  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-hom 15966  df-cco 15967  df-cat 16329  df-cid 16330  df-oppc 16372  df-mon 16390  df-epi 16391  df-setc 16726

This theorem is referenced by: (None)