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

Theorem setcepi 17801
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 (𝜑 → 2o𝑈)
Assertion
Ref Expression
setcepi (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋onto𝑌))

Proof of Theorem setcepi
Dummy variables 𝑥 𝑔 𝑎 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2740 . . . . . 6 (Base‘𝐶) = (Base‘𝐶)
2 eqid 2740 . . . . . 6 (Hom ‘𝐶) = (Hom ‘𝐶)
3 eqid 2740 . . . . . 6 (comp‘𝐶) = (comp‘𝐶)
4 setcepi.h . . . . . 6 𝐸 = (Epi‘𝐶)
5 setcmon.u . . . . . . 7 (𝜑𝑈𝑉)
6 setcmon.c . . . . . . . 8 𝐶 = (SetCat‘𝑈)
76setccat 17798 . . . . . . 7 (𝑈𝑉𝐶 ∈ Cat)
85, 7syl 17 . . . . . 6 (𝜑𝐶 ∈ Cat)
9 setcmon.x . . . . . . 7 (𝜑𝑋𝑈)
106, 5setcbas 17791 . . . . . . 7 (𝜑𝑈 = (Base‘𝐶))
119, 10eleqtrd 2843 . . . . . 6 (𝜑𝑋 ∈ (Base‘𝐶))
12 setcmon.y . . . . . . 7 (𝜑𝑌𝑈)
1312, 10eleqtrd 2843 . . . . . 6 (𝜑𝑌 ∈ (Base‘𝐶))
141, 2, 3, 4, 8, 11, 13epihom 17452 . . . . 5 (𝜑 → (𝑋𝐸𝑌) ⊆ (𝑋(Hom ‘𝐶)𝑌))
1514sselda 3926 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
166, 5, 2, 9, 12elsetchom 17794 . . . . 5 (𝜑 → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ↔ 𝐹:𝑋𝑌))
1716biimpa 477 . . . 4 ((𝜑𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) → 𝐹:𝑋𝑌)
1815, 17syldan 591 . . 3 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹:𝑋𝑌)
1918frnd 6606 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹𝑌)
2018ffnd 6599 . . . . . . . . . . . . . 14 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 Fn 𝑋)
21 fnfvelrn 6955 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝑋𝑥𝑋) → (𝐹𝑥) ∈ ran 𝐹)
2220, 21sylan 580 . . . . . . . . . . . . 13 (((𝜑𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥𝑋) → (𝐹𝑥) ∈ ran 𝐹)
2322iftrued 4473 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥𝑋) → if((𝐹𝑥) ∈ ran 𝐹, 1o, ∅) = 1o)
2423mpteq2dva 5179 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑥𝑋 ↦ if((𝐹𝑥) ∈ ran 𝐹, 1o, ∅)) = (𝑥𝑋 ↦ 1o))
2518ffvelrnda 6958 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐸𝑌)) ∧ 𝑥𝑋) → (𝐹𝑥) ∈ 𝑌)
2618feqmptd 6834 . . . . . . . . . . . 12 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 = (𝑥𝑋 ↦ (𝐹𝑥)))
27 eqidd 2741 . . . . . . . . . . . 12 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)))
28 eleq1 2828 . . . . . . . . . . . . 13 (𝑎 = (𝐹𝑥) → (𝑎 ∈ ran 𝐹 ↔ (𝐹𝑥) ∈ ran 𝐹))
2928ifbid 4488 . . . . . . . . . . . 12 (𝑎 = (𝐹𝑥) → if(𝑎 ∈ ran 𝐹, 1o, ∅) = if((𝐹𝑥) ∈ ran 𝐹, 1o, ∅))
3025, 26, 27, 29fmptco 6998 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∘ 𝐹) = (𝑥𝑋 ↦ if((𝐹𝑥) ∈ ran 𝐹, 1o, ∅)))
31 fconstmpt 5650 . . . . . . . . . . . . 13 (𝑌 × {1o}) = (𝑎𝑌 ↦ 1o)
3231a1i 11 . . . . . . . . . . . 12 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1o}) = (𝑎𝑌 ↦ 1o))
33 eqidd 2741 . . . . . . . . . . . 12 (𝑎 = (𝐹𝑥) → 1o = 1o)
3425, 26, 32, 33fmptco 6998 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1o}) ∘ 𝐹) = (𝑥𝑋 ↦ 1o))
3524, 30, 343eqtr4d 2790 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∘ 𝐹) = ((𝑌 × {1o}) ∘ 𝐹))
365adantr 481 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑈𝑉)
379adantr 481 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋𝑈)
3812adantr 481 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌𝑈)
39 setcepi.2 . . . . . . . . . . . 12 (𝜑 → 2o𝑈)
4039adantr 481 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 2o𝑈)
41 eqid 2740 . . . . . . . . . . . . 13 (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅))
42 1oex 8298 . . . . . . . . . . . . . . . . 17 1o ∈ V
4342prid2 4705 . . . . . . . . . . . . . . . 16 1o ∈ {∅, 1o}
44 df2o3 8296 . . . . . . . . . . . . . . . 16 2o = {∅, 1o}
4543, 44eleqtrri 2840 . . . . . . . . . . . . . . 15 1o ∈ 2o
46 0ex 5235 . . . . . . . . . . . . . . . . 17 ∅ ∈ V
4746prid1 4704 . . . . . . . . . . . . . . . 16 ∅ ∈ {∅, 1o}
4847, 44eleqtrri 2840 . . . . . . . . . . . . . . 15 ∅ ∈ 2o
4945, 48ifcli 4512 . . . . . . . . . . . . . 14 if(𝑎 ∈ ran 𝐹, 1o, ∅) ∈ 2o
5049a1i 11 . . . . . . . . . . . . 13 (𝑎𝑌 → if(𝑎 ∈ ran 𝐹, 1o, ∅) ∈ 2o)
5141, 50fmpti 6983 . . . . . . . . . . . 12 (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)):𝑌⟶2o
5251a1i 11 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)):𝑌⟶2o)
536, 36, 3, 37, 38, 40, 18, 52setcco 17796 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅))(⟨𝑋, 𝑌⟩(comp‘𝐶)2o)𝐹) = ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∘ 𝐹))
54 fconst6g 6661 . . . . . . . . . . . 12 (1o ∈ 2o → (𝑌 × {1o}):𝑌⟶2o)
5545, 54mp1i 13 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1o}):𝑌⟶2o)
566, 36, 3, 37, 38, 40, 18, 55setcco 17796 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1o})(⟨𝑋, 𝑌⟩(comp‘𝐶)2o)𝐹) = ((𝑌 × {1o}) ∘ 𝐹))
5735, 53, 563eqtr4d 2790 . . . . . . . . 9 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅))(⟨𝑋, 𝑌⟩(comp‘𝐶)2o)𝐹) = ((𝑌 × {1o})(⟨𝑋, 𝑌⟩(comp‘𝐶)2o)𝐹))
588adantr 481 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐶 ∈ Cat)
5911adantr 481 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑋 ∈ (Base‘𝐶))
6013adantr 481 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ∈ (Base‘𝐶))
6139, 10eleqtrd 2843 . . . . . . . . . . 11 (𝜑 → 2o ∈ (Base‘𝐶))
6261adantr 481 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 2o ∈ (Base‘𝐶))
63 simpr 485 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹 ∈ (𝑋𝐸𝑌))
646, 36, 2, 38, 40elsetchom 17794 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∈ (𝑌(Hom ‘𝐶)2o) ↔ (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)):𝑌⟶2o))
6552, 64mpbird 256 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) ∈ (𝑌(Hom ‘𝐶)2o))
666, 36, 2, 38, 40elsetchom 17794 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ((𝑌 × {1o}) ∈ (𝑌(Hom ‘𝐶)2o) ↔ (𝑌 × {1o}):𝑌⟶2o))
6755, 66mpbird 256 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑌 × {1o}) ∈ (𝑌(Hom ‘𝐶)2o))
681, 2, 3, 4, 58, 59, 60, 62, 63, 65, 67epii 17453 . . . . . . . . 9 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅))(⟨𝑋, 𝑌⟩(comp‘𝐶)2o)𝐹) = ((𝑌 × {1o})(⟨𝑋, 𝑌⟩(comp‘𝐶)2o)𝐹) ↔ (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑌 × {1o})))
6957, 68mpbid 231 . . . . . . . 8 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑌 × {1o}))
7069, 31eqtrdi 2796 . . . . . . 7 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → (𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎𝑌 ↦ 1o))
7149rgenw 3078 . . . . . . . 8 𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) ∈ 2o
72 mpteqb 6891 . . . . . . . 8 (∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) ∈ 2o → ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎𝑌 ↦ 1o) ↔ ∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o))
7371, 72ax-mp 5 . . . . . . 7 ((𝑎𝑌 ↦ if(𝑎 ∈ ran 𝐹, 1o, ∅)) = (𝑎𝑌 ↦ 1o) ↔ ∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o)
7470, 73sylib 217 . . . . . 6 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o)
75 1n0 8309 . . . . . . . . . 10 1o ≠ ∅
7675nesymi 3003 . . . . . . . . 9 ¬ ∅ = 1o
77 iffalse 4474 . . . . . . . . . 10 𝑎 ∈ ran 𝐹 → if(𝑎 ∈ ran 𝐹, 1o, ∅) = ∅)
7877eqeq1d 2742 . . . . . . . . 9 𝑎 ∈ ran 𝐹 → (if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o ↔ ∅ = 1o))
7976, 78mtbiri 327 . . . . . . . 8 𝑎 ∈ ran 𝐹 → ¬ if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o)
8079con4i 114 . . . . . . 7 (if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o𝑎 ∈ ran 𝐹)
8180ralimi 3089 . . . . . 6 (∀𝑎𝑌 if(𝑎 ∈ ran 𝐹, 1o, ∅) = 1o → ∀𝑎𝑌 𝑎 ∈ ran 𝐹)
8274, 81syl 17 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ∀𝑎𝑌 𝑎 ∈ ran 𝐹)
83 dfss3 3914 . . . . 5 (𝑌 ⊆ ran 𝐹 ↔ ∀𝑎𝑌 𝑎 ∈ ran 𝐹)
8482, 83sylibr 233 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝑌 ⊆ ran 𝐹)
8519, 84eqssd 3943 . . 3 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → ran 𝐹 = 𝑌)
86 dffo2 6690 . . 3 (𝐹:𝑋onto𝑌 ↔ (𝐹:𝑋𝑌 ∧ ran 𝐹 = 𝑌))
8718, 85, 86sylanbrc 583 . 2 ((𝜑𝐹 ∈ (𝑋𝐸𝑌)) → 𝐹:𝑋onto𝑌)
88 fof 6686 . . . . 5 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
8988adantl 482 . . . 4 ((𝜑𝐹:𝑋onto𝑌) → 𝐹:𝑋𝑌)
9016biimpar 478 . . . 4 ((𝜑𝐹:𝑋𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
9189, 90syldan 591 . . 3 ((𝜑𝐹:𝑋onto𝑌) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
9210adantr 481 . . . . . 6 ((𝜑𝐹:𝑋onto𝑌) → 𝑈 = (Base‘𝐶))
9392eleq2d 2826 . . . . 5 ((𝜑𝐹:𝑋onto𝑌) → (𝑧𝑈𝑧 ∈ (Base‘𝐶)))
945ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑈𝑉)
959ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑋𝑈)
9612ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑌𝑈)
97 simprl 768 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑧𝑈)
9889adantr 481 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋𝑌)
99 simprrl 778 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧))
1006, 94, 2, 96, 97elsetchom 17794 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ 𝑔:𝑌𝑧))
10199, 100mpbid 231 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔:𝑌𝑧)
1026, 94, 3, 95, 96, 97, 98, 101setcco 17796 . . . . . . . . . 10 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (𝑔𝐹))
103 simprrr 779 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ∈ (𝑌(Hom ‘𝐶)𝑧))
1046, 94, 2, 96, 97elsetchom 17794 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ( ∈ (𝑌(Hom ‘𝐶)𝑧) ↔ :𝑌𝑧))
105103, 104mpbid 231 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → :𝑌𝑧)
1066, 94, 3, 95, 96, 97, 98, 105setcco 17796 . . . . . . . . . 10 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = (𝐹))
107102, 106eqeq12d 2756 . . . . . . . . 9 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) ↔ (𝑔𝐹) = (𝐹)))
108 simplr 766 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝐹:𝑋onto𝑌)
109101ffnd 6599 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → 𝑔 Fn 𝑌)
110105ffnd 6599 . . . . . . . . . . 11 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → Fn 𝑌)
111 cocan2 7160 . . . . . . . . . . 11 ((𝐹:𝑋onto𝑌𝑔 Fn 𝑌 Fn 𝑌) → ((𝑔𝐹) = (𝐹) ↔ 𝑔 = ))
112108, 109, 110, 111syl3anc 1370 . . . . . . . . . 10 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔𝐹) = (𝐹) ↔ 𝑔 = ))
113112biimpd 228 . . . . . . . . 9 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔𝐹) = (𝐹) → 𝑔 = ))
114107, 113sylbid 239 . . . . . . . 8 (((𝜑𝐹:𝑋onto𝑌) ∧ (𝑧𝑈 ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧)))) → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))
115114anassrs 468 . . . . . . 7 ((((𝜑𝐹:𝑋onto𝑌) ∧ 𝑧𝑈) ∧ (𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧) ∧ ∈ (𝑌(Hom ‘𝐶)𝑧))) → ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))
116115ralrimivva 3117 . . . . . 6 (((𝜑𝐹:𝑋onto𝑌) ∧ 𝑧𝑈) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))
117116ex 413 . . . . 5 ((𝜑𝐹:𝑋onto𝑌) → (𝑧𝑈 → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = )))
11893, 117sylbird 259 . . . 4 ((𝜑𝐹:𝑋onto𝑌) → (𝑧 ∈ (Base‘𝐶) → ∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = )))
119118ralrimiv 3109 . . 3 ((𝜑𝐹:𝑋onto𝑌) → ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))
1201, 2, 3, 4, 8, 11, 13isepi2 17451 . . . 4 (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))))
121120adantr 481 . . 3 ((𝜑𝐹:𝑋onto𝑌) → (𝐹 ∈ (𝑋𝐸𝑌) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑌(Hom ‘𝐶)𝑧)∀ ∈ (𝑌(Hom ‘𝐶)𝑧)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) = ((⟨𝑋, 𝑌⟩(comp‘𝐶)𝑧)𝐹) → 𝑔 = ))))
12291, 119, 121mpbir2and 710 . 2 ((𝜑𝐹:𝑋onto𝑌) → 𝐹 ∈ (𝑋𝐸𝑌))
12387, 122impbida 798 1 (𝜑 → (𝐹 ∈ (𝑋𝐸𝑌) ↔ 𝐹:𝑋onto𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1542  wcel 2110  wral 3066  wss 3892  c0 4262  ifcif 4465  {csn 4567  {cpr 4569  cop 4573  cmpt 5162   × cxp 5588  ran crn 5591  ccom 5594   Fn wfn 6427  wf 6428  ontowfo 6430  cfv 6432  (class class class)co 7271  1oc1o 8281  2oc2o 8282  Basecbs 16910  Hom chom 16971  compcco 16972  Catccat 17371  Epicepi 17439  SetCatcsetc 17788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-cnex 10928  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948  ax-pre-mulgt0 10949
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-om 7707  df-1st 7824  df-2nd 7825  df-tpos 8033  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-1o 8288  df-2o 8289  df-er 8481  df-map 8600  df-en 8717  df-dom 8718  df-sdom 8719  df-fin 8720  df-pnf 11012  df-mnf 11013  df-xr 11014  df-ltxr 11015  df-le 11016  df-sub 11207  df-neg 11208  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12437  df-uz 12582  df-fz 13239  df-struct 16846  df-sets 16863  df-slot 16881  df-ndx 16893  df-base 16911  df-hom 16984  df-cco 16985  df-cat 17375  df-cid 17376  df-oppc 17419  df-mon 17440  df-epi 17441  df-setc 17789
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator