MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  setcepi Structured version   Visualization version   GIF version

Theorem setcepi 17003
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.
StepHypRef Expression
1 eqid 2765 . . . . . 6 (Base‘𝐶) = (Base‘𝐶)
2 eqid 2765 . . . . . 6 (Hom ‘𝐶) = (Hom ‘𝐶)
3 eqid 2765 . . . . . 6 (comp‘𝐶) = (comp‘𝐶)
4 setcepi.h . . . . . 6 𝐸 = (Epi‘𝐶)
5 setcmon.u . . . . . . 7 (𝜑𝑈𝑉)
6 setcmon.c . . . . . . . 8 𝐶 = (SetCat‘𝑈)
76setccat 17000 . . . . . . 7 (𝑈𝑉𝐶 ∈ Cat)
85, 7syl 17 . . . . . 6 (𝜑𝐶 ∈ Cat)
9 setcmon.x . . . . . . 7 (𝜑𝑋𝑈)
106, 5setcbas 16993 . . . . . . 7 (𝜑𝑈 = (Base‘𝐶))
119, 10eleqtrd 2846 . . . . . 6 (𝜑𝑋 ∈ (Base‘𝐶))
12 setcmon.y . . . . . . 7 (𝜑𝑌𝑈)
1312, 10eleqtrd 2846 . . . . . 6 (𝜑𝑌 ∈ (Base‘𝐶))
141, 2, 3, 4, 8, 11, 13epihom 16667 . . . . 5 (𝜑 → (𝑋𝐸𝑌) ⊆ (𝑋(Hom ‘𝐶)𝑌))
1514sselda 3761 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
166, 5, 2, 9, 12elsetchom 16996 . . . . 5 (𝜑 → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ↔ 𝐹:𝑋𝑌))
1716biimpa 468 . . . 4 ((𝜑𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) → 𝐹:𝑋𝑌)
1815, 17syldan 585 . . 3 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹:𝑋𝑌)
1918frnd 6230 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹𝑌)
2018ffnd 6224 . . . . . . . . . . . . . 14 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 Fn 𝑋)
21 fnfvelrn 6546 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝑋𝑥𝑋) → (𝐹𝑥) ∈ ran 𝐹)
2220, 21sylan 575 . . . . . . . . . . . . 13 (((𝜑𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥𝑋) → (𝐹𝑥) ∈ ran 𝐹)
2322iftrued 4251 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥𝑋) → if((𝐹𝑥) ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜)
2423mpteq2dva 4903 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑥𝑋 ↦ if((𝐹𝑥) ∈ ran 𝐹, 1𝑜, ∅)) = (𝑥𝑋 ↦ 1𝑜))
2518ffvelrnda 6549 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥𝑋) → (𝐹𝑥) ∈ 𝑌)
2618feqmptd 6438 . . . . . . . . . . . 12 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 = (𝑥𝑋 ↦ (𝐹𝑥)))
27 eqidd 2766 . . . . . . . . . . . 12 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)))
28 eleq1 2832 . . . . . . . . . . . . 13 (𝑎 = (𝐹𝑥) → (𝑎 ∈ ran 𝐹 ↔ (𝐹𝑥) ∈ ran 𝐹))
2928ifbid 4265 . . . . . . . . . . . 12 (𝑎 = (𝐹𝑥) → if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = if((𝐹𝑥) ∈ ran 𝐹, 1𝑜, ∅))
3025, 26, 27, 29fmptco 6587 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∘ 𝐹) = (𝑥𝑋 ↦ if((𝐹𝑥) ∈ ran 𝐹, 1𝑜, ∅)))
31 fconstmpt 5333 . . . . . . . . . . . . 13 (𝑌 × {1𝑜}) = (𝑎𝑌 ↦ 1𝑜)
3231a1i 11 . . . . . . . . . . . 12 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1𝑜}) = (𝑎𝑌 ↦ 1𝑜))
33 eqidd 2766 . . . . . . . . . . . 12 (𝑎 = (𝐹𝑥) → 1𝑜 = 1𝑜)
3425, 26, 32, 33fmptco 6587 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1𝑜}) ∘ 𝐹) = (𝑥𝑋 ↦ 1𝑜))
3524, 30, 343eqtr4d 2809 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∘ 𝐹) = ((𝑌 × {1𝑜}) ∘ 𝐹))
365adantr 472 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑈𝑉)
379adantr 472 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋𝑈)
3812adantr 472 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌𝑈)
39 setcepi.2 . . . . . . . . . . . 12 (𝜑 → 2𝑜𝑈)
4039adantr 472 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 2𝑜𝑈)
41 eqid 2765 . . . . . . . . . . . . 13 (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅))
42 1onn 7924 . . . . . . . . . . . . . . . . . 18 1𝑜 ∈ ω
4342elexi 3366 . . . . . . . . . . . . . . . . 17 1𝑜 ∈ V
4443prid2 4453 . . . . . . . . . . . . . . . 16 1𝑜 ∈ {∅, 1𝑜}
45 df2o3 7778 . . . . . . . . . . . . . . . 16 2𝑜 = {∅, 1𝑜}
4644, 45eleqtrri 2843 . . . . . . . . . . . . . . 15 1𝑜 ∈ 2𝑜
47 0ex 4950 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
4847prid1 4452 . . . . . . . . . . . . . . . 16 ∅ ∈ {∅, 1𝑜}
4948, 45eleqtrri 2843 . . . . . . . . . . . . . . 15 ∅ ∈ 2𝑜
5046, 49ifcli 4289 . . . . . . . . . . . . . 14 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈ 2𝑜
5150a1i 11 . . . . . . . . . . . . 13 (𝑎𝑌 → if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈ 2𝑜)
5241, 51fmpti 6572 . . . . . . . . . . . 12 (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)):𝑌⟶2𝑜
5352a1i 11 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)):𝑌⟶2𝑜)
546, 36, 3, 37, 38, 40, 18, 53setcco 16998 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅))(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) = ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∘ 𝐹))
55 fconst6g 6276 . . . . . . . . . . . 12 (1𝑜 ∈ 2𝑜 → (𝑌 × {1𝑜}):𝑌⟶2𝑜)
5646, 55mp1i 13 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1𝑜}):𝑌⟶2𝑜)
576, 36, 3, 37, 38, 40, 18, 56setcco 16998 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1𝑜})(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) = ((𝑌 × {1𝑜}) ∘ 𝐹))
5835, 54, 573eqtr4d 2809 . . . . . . . . 9 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅))(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) = ((𝑌 × {1𝑜})(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹))
598adantr 472 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐶 ∈ Cat)
6011adantr 472 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋 ∈ (Base‘𝐶))
6113adantr 472 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ∈ (Base‘𝐶))
6239, 10eleqtrd 2846 . . . . . . . . . . 11 (𝜑 → 2𝑜 ∈ (Base‘𝐶))
6362adantr 472 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 2𝑜 ∈ (Base‘𝐶))
64 simpr 477 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 ∈ (𝑋𝐸𝑌))
656, 36, 2, 38, 40elsetchom 16996 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∈ (𝑌(Hom ‘𝐶)2𝑜) ↔ (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)):𝑌⟶2𝑜))
6653, 65mpbird 248 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) ∈ (𝑌(Hom ‘𝐶)2𝑜))
676, 36, 2, 38, 40elsetchom 16996 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1𝑜}) ∈ (𝑌(Hom ‘𝐶)2𝑜) ↔ (𝑌 × {1𝑜}):𝑌⟶2𝑜))
6856, 67mpbird 248 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1𝑜}) ∈ (𝑌(Hom ‘𝐶)2𝑜))
691, 2, 3, 4, 59, 60, 61, 63, 64, 66, 68epii 16668 . . . . . . . . 9 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅))(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) = ((𝑌 × {1𝑜})(⟨𝑋, 𝑌⟩(comp‘𝐶)2𝑜)𝐹) ↔ (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑌 × {1𝑜})))
7058, 69mpbid 223 . . . . . . . 8 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑌 × {1𝑜}))
7170, 31syl6eq 2815 . . . . . . 7 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎𝑌 ↦ 1𝑜))
7250rgenw 3071 . . . . . . . 8 𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈ 2𝑜
73 mpteqb 6488 . . . . . . . 8 (∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) ∈ 2𝑜 → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎𝑌 ↦ 1𝑜) ↔ ∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜))
7472, 73ax-mp 5 . . . . . . 7 ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅)) = (𝑎𝑌 ↦ 1𝑜) ↔ ∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜)
7571, 74sylib 209 . . . . . 6 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜)
76 1n0 7780 . . . . . . . . . 10 1𝑜 ≠ ∅
7776nesymi 2994 . . . . . . . . 9 ¬ ∅ = 1𝑜
78 iffalse 4252 . . . . . . . . . 10 𝑎 ∈ ran 𝐹 → if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = ∅)
7978eqeq1d 2767 . . . . . . . . 9 𝑎 ∈ ran 𝐹 → (if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜 ↔ ∅ = 1𝑜))
8077, 79mtbiri 318 . . . . . . . 8 𝑎 ∈ ran 𝐹 → ¬ if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜)
8180con4i 114 . . . . . . 7 (if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜𝑎 ∈ ran 𝐹)
8281ralimi 3099 . . . . . 6 (∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1𝑜, ∅) = 1𝑜 → ∀𝑎𝑌 𝑎 ∈ ran 𝐹)
8375, 82syl 17 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎𝑌 𝑎 ∈ ran 𝐹)
84 dfss3 3750 . . . . 5 (𝑌 ⊆ ran 𝐹 ↔ ∀𝑎𝑌 𝑎 ∈ ran 𝐹)
8583, 84sylibr 225 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ⊆ ran 𝐹)
8619, 85eqssd 3778 . . 3 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹 = 𝑌)
87 dffo2 6302 . . 3 (𝐹:𝑋onto𝑌 ↔ (𝐹:𝑋𝑌 ∧ ran 𝐹 = 𝑌))
8818, 86, 87sylanbrc 578 . 2 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹:𝑋onto𝑌)
89 fof 6298 . . . . 5 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
9089adantl 473 . . . 4 ((𝜑𝐹:𝑋onto𝑌) → 𝐹:𝑋𝑌)
9116biimpar 469 . . . 4 ((𝜑𝐹:𝑋𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
9290, 91syldan 585 . . 3 ((𝜑𝐹:𝑋onto𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
9310adantr 472 . . . . . 6 ((𝜑𝐹:𝑋onto𝑌) → 𝑈 = (Base‘𝐶))
9493eleq2d 2830 . . . . 5 ((𝜑𝐹:𝑋onto𝑌) → (𝑧𝑈𝑧 ∈ (Base‘𝐶)))
955ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑈𝑉)
969ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑋𝑈)
9712ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑌𝑈)
98 simprl 787 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑧𝑈)
9990adantr 472 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋𝑌)
100 simprrl 799 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧))
1016, 95, 2, 97, 98elsetchom 16996 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ 𝑔:𝑌𝑧))
102100, 101mpbid 223 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔:𝑌𝑧)
1036, 95, 3, 96, 97, 98, 99, 102setcco 16998 . . . . . . . . . 10 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (𝑔𝐹))
104 simprrr 800 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ∈ (𝑌(Hom ‘𝐶)𝑧))
1056, 95, 2, 97, 98elsetchom 16996 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ( ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ :𝑌𝑧))
106104, 105mpbid 223 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → :𝑌𝑧)
1076, 95, 3, 96, 97, 98, 99, 106setcco 16998 . . . . . . . . . 10 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (𝐹))
108103, 107eqeq12d 2780 . . . . . . . . 9 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) ↔ (𝑔𝐹) = (𝐹)))
109 simplr 785 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋onto𝑌)
110102ffnd 6224 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 Fn 𝑌)
111106ffnd 6224 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → Fn 𝑌)
112 cocan2 6739 . . . . . . . . . . 11 ((𝐹:𝑋onto𝑌𝑔 Fn 𝑌 Fn 𝑌) → ((𝑔𝐹) = (𝐹) ↔ 𝑔 = ))
113109, 110, 111, 112syl3anc 1490 . . . . . . . . . 10 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔𝐹) = (𝐹) ↔ 𝑔 = ))
114113biimpd 220 . . . . . . . . 9 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔𝐹) = (𝐹) → 𝑔 = ))
115108, 114sylbid 231 . . . . . . . 8 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))
116115anassrs 459 . . . . . . 7 ((((𝜑𝐹:𝑋onto𝑌) ∧ 𝑧𝑈) ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))
117116ralrimivva 3118 . . . . . 6 (((𝜑𝐹:𝑋onto𝑌) ∧ 𝑧𝑈) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))
118117ex 401 . . . . 5 ((𝜑𝐹:𝑋onto𝑌) → (𝑧𝑈 → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = )))
11994, 118sylbird 251 . . . 4 ((𝜑𝐹:𝑋onto𝑌) → (𝑧 ∈ (Base‘𝐶) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = )))
120119ralrimiv 3112 . . 3 ((𝜑𝐹:𝑋onto𝑌) → ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))
1211, 2, 3, 4, 8, 11, 13isepi2 16666 . . . 4 (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))))
122121adantr 472 . . 3 ((𝜑𝐹:𝑋onto𝑌) → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))))
12392, 120, 122mpbir2and 704 . 2 ((𝜑𝐹:𝑋onto𝑌) → 𝐹 ∈ (𝑋𝐸𝑌))
12488, 123impbida 835 1 (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋onto𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  wss 3732  c0 4079  ifcif 4243  {csn 4334  {cpr 4336  cop 4340  cmpt 4888   × cxp 5275  ran crn 5278  ccom 5281   Fn wfn 6063  wf 6064  ontowfo 6066  cfv 6068  (class class class)co 6842  ωcom 7263  1𝑜c1o 7757  2𝑜c2o 7758  Basecbs 16130  Hom chom 16225  compcco 16226  Catccat 16590  Epicepi 16654  SetCatcsetc 16990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-tpos 7555  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-fz 12534  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-hom 16238  df-cco 16239  df-cat 16594  df-cid 16595  df-oppc 16637  df-mon 16655  df-epi 16656  df-setc 16991
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator