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 𝐶 = ( SetCat ‘ 𝑈 )
setcmon.u ( 𝜑𝑈𝑉 )
setcmon.x ( 𝜑𝑋𝑈 )
setcmon.y ( 𝜑𝑌𝑈 )
setcepi.h 𝐸 = ( Epi ‘ 𝐶 )
setcepi.2 ( 𝜑 → 2o𝑈 )
Assertion setcepi ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ 𝐹 : 𝑋onto𝑌 ) )

Proof

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