Metamath Proof Explorer

Theorem 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 
|- ( ph -> U e. V )
setcmon.x 
|- ( ph -> X e. U )
setcmon.y 
|- ( ph -> Y e. U )
setcepi.h 
|- E = ( Epi ` C )
setcepi.2 
|- ( ph -> 2o e. U )
Assertion setcepi 
|- ( ph -> ( F e. ( X E Y ) <-> F : X -onto-> Y ) )

Proof

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