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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 )
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 1oelpr ⊢ 1o ∈ { ∅ , 1o }
43 df2o3 ⊢ 2o = { ∅ , 1o }
44 42 43 eleqtrri ⊢ 1o ∈ 2o
45 0ex ⊢ ∅ ∈ V
46 45 prid1 ⊢ ∅ ∈ { ∅ , 1o }
47 46 43 eleqtrri ⊢ ∅ ∈ 2o
48 44 47 ifcli ⊢ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ∈ 2o
49 48 a1i ⊢ ( 𝑎 ∈ 𝑌 → if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ∈ 2o )
50 41 49 fmpti ⊢ ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) : 𝑌 ⟶ 2o
51 50 a1i ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) : 𝑌 ⟶ 2o )
52 1 37 9 38 39 40 19 51 setcco ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 2o ) 𝐹 ) = ( ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) ∘ 𝐹 ) )
53 fconst6g ⊢ ( 1o ∈ 2o → ( 𝑌 × { 1o } ) : 𝑌 ⟶ 2o )
54 44 53 mp1i ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( 𝑌 × { 1o } ) : 𝑌 ⟶ 2o )
55 1 37 9 38 39 40 19 54 setcco ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( ( 𝑌 × { 1o } ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 2o ) 𝐹 ) = ( ( 𝑌 × { 1o } ) ∘ 𝐹 ) )
56 36 52 55 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 2o ) 𝐹 ) = ( ( 𝑌 × { 1o } ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 2o ) 𝐹 ) )
57 11 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → 𝐶 ∈ Cat )
58 13 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
59 14 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
60 6 12 eleqtrd ⊢ ( 𝜑 → 2o ∈ ( Base ‘ 𝐶 ) )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → 2o ∈ ( Base ‘ 𝐶 ) )
62 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) )
63 1 37 8 39 40 elsetchom ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 2o ) ↔ ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) : 𝑌 ⟶ 2o ) )
64 51 63 mpbird ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 2o ) )
65 1 37 8 39 40 elsetchom ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( ( 𝑌 × { 1o } ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 2o ) ↔ ( 𝑌 × { 1o } ) : 𝑌 ⟶ 2o ) )
66 54 65 mpbird ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( 𝑌 × { 1o } ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 2o ) )
67 7 8 9 5 57 58 59 61 62 64 66 epii ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( ( ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 2o ) 𝐹 ) = ( ( 𝑌 × { 1o } ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 2o ) 𝐹 ) ↔ ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) = ( 𝑌 × { 1o } ) ) )
68 56 67 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) = ( 𝑌 × { 1o } ) )
69 68 32 eqtrdi ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) = ( 𝑎 ∈ 𝑌 ↦ 1o ) )
70 48 rgenw ⊢ ∀ 𝑎 ∈ 𝑌 if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ∈ 2o
71 mpteqb ⊢ ( ∀ 𝑎 ∈ 𝑌 if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ∈ 2o → ( ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) = ( 𝑎 ∈ 𝑌 ↦ 1o ) ↔ ∀ 𝑎 ∈ 𝑌 if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) = 1o ) )
72 70 71 ax-mp ⊢ ( ( 𝑎 ∈ 𝑌 ↦ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) ) = ( 𝑎 ∈ 𝑌 ↦ 1o ) ↔ ∀ 𝑎 ∈ 𝑌 if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) = 1o )
73 69 72 sylib ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ∀ 𝑎 ∈ 𝑌 if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) = 1o )
74 1n0 ⊢ 1o ≠ ∅
75 74 nesymi ⊢ ¬ ∅ = 1o
76 iffalse ⊢ ( ¬ 𝑎 ∈ ran 𝐹 → if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) = ∅ )
77 76 eqeq1d ⊢ ( ¬ 𝑎 ∈ ran 𝐹 → ( if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) = 1o ↔ ∅ = 1o ) )
78 75 77 mtbiri ⊢ ( ¬ 𝑎 ∈ ran 𝐹 → ¬ if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) = 1o )
79 78 con4i ⊢ ( if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) = 1o → 𝑎 ∈ ran 𝐹 )
80 79 ralimi ⊢ ( ∀ 𝑎 ∈ 𝑌 if ( 𝑎 ∈ ran 𝐹 , 1o , ∅ ) = 1o → ∀ 𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹 )
81 73 80 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ∀ 𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹 )
82 dfss3 ⊢ ( 𝑌 ⊆ ran 𝐹 ↔ ∀ 𝑎 ∈ 𝑌 𝑎 ∈ ran 𝐹 )
83 81 82 sylibr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → 𝑌 ⊆ ran 𝐹 )
84 20 83 eqssd ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → ran 𝐹 = 𝑌 )
85 dffo2 ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ran 𝐹 = 𝑌 ) )
86 19 84 85 sylanbrc ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) → 𝐹 : 𝑋 –onto→ 𝑌 )
87 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
88 87 adantl ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
89 17 biimpar ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
90 88 89 syldan ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
91 12 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝑈 = ( Base ‘ 𝐶 ) )
92 91 eleq2d ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑧 ∈ 𝑈 ↔ 𝑧 ∈ ( Base ‘ 𝐶 ) ) )
93 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑈 ∈ 𝑉 )
94 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑋 ∈ 𝑈 )
95 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑌 ∈ 𝑈 )
96 simprl ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑧 ∈ 𝑈 )
97 88 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
98 simprrl ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) )
99 1 93 8 95 96 elsetchom ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ↔ 𝑔 : 𝑌 ⟶ 𝑧 ) )
100 98 99 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 : 𝑌 ⟶ 𝑧 )
101 1 93 9 94 95 96 97 100 setcco ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( 𝑔 ∘ 𝐹 ) )
102 simprrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) )
103 1 93 8 95 96 elsetchom ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ↔ ℎ : 𝑌 ⟶ 𝑧 ) )
104 102 103 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ℎ : 𝑌 ⟶ 𝑧 )
105 1 93 9 94 95 96 97 104 setcco ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ∘ 𝐹 ) )
106 101 105 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) ↔ ( 𝑔 ∘ 𝐹 ) = ( ℎ ∘ 𝐹 ) ) )
107 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝐹 : 𝑋 –onto→ 𝑌 )
108 100 ffnd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 Fn 𝑌 )
109 104 ffnd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ℎ Fn 𝑌 )
110 cocan2 ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑔 Fn 𝑌 ∧ ℎ Fn 𝑌 ) → ( ( 𝑔 ∘ 𝐹 ) = ( ℎ ∘ 𝐹 ) ↔ 𝑔 = ℎ ) )
111 107 108 109 110 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔 ∘ 𝐹 ) = ( ℎ ∘ 𝐹 ) ↔ 𝑔 = ℎ ) )
112 111 biimpd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔 ∘ 𝐹 ) = ( ℎ ∘ 𝐹 ) → 𝑔 = ℎ ) )
113 106 112 sylbid ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ ( 𝑧 ∈ 𝑈 ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) )
114 113 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) )
115 114 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) ∧ 𝑧 ∈ 𝑈 ) → ∀ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) )
116 115 ex ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑧 ∈ 𝑈 → ∀ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) )
117 92 116 sylbird ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑧 ∈ ( Base ‘ 𝐶 ) → ∀ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) )
118 117 ralrimiv ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) )
119 7 8 9 5 11 13 14 isepi2 ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) ) )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑔 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝐹 ) → 𝑔 = ℎ ) ) ) )
121 90 118 120 mpbir2and ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) )
122 86 121 impbida ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ 𝐹 : 𝑋 –onto→ 𝑌 ) )