Metamath Proof Explorer


Theorem isepi

Description: Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses isepi.b 𝐵 = ( Base ‘ 𝐶 )
isepi.h 𝐻 = ( Hom ‘ 𝐶 )
isepi.o · = ( comp ‘ 𝐶 )
isepi.e 𝐸 = ( Epi ‘ 𝐶 )
isepi.c ( 𝜑𝐶 ∈ Cat )
isepi.x ( 𝜑𝑋𝐵 )
isepi.y ( 𝜑𝑌𝐵 )
Assertion isepi ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑧 ) 𝐹 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isepi.b 𝐵 = ( Base ‘ 𝐶 )
2 isepi.h 𝐻 = ( Hom ‘ 𝐶 )
3 isepi.o · = ( comp ‘ 𝐶 )
4 isepi.e 𝐸 = ( Epi ‘ 𝐶 )
5 isepi.c ( 𝜑𝐶 ∈ Cat )
6 isepi.x ( 𝜑𝑋𝐵 )
7 isepi.y ( 𝜑𝑌𝐵 )
8 eqid ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
9 8 1 oppcbas 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) )
10 eqid ( Hom ‘ ( oppCat ‘ 𝐶 ) ) = ( Hom ‘ ( oppCat ‘ 𝐶 ) )
11 eqid ( comp ‘ ( oppCat ‘ 𝐶 ) ) = ( comp ‘ ( oppCat ‘ 𝐶 ) )
12 eqid ( Mono ‘ ( oppCat ‘ 𝐶 ) ) = ( Mono ‘ ( oppCat ‘ 𝐶 ) )
13 8 oppccat ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat )
14 5 13 syl ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat )
15 9 10 11 12 14 7 6 ismon ( 𝜑 → ( 𝐹 ∈ ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ↔ ( 𝐹 ∈ ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ∧ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) ) ) )
16 8 5 12 4 oppcmon ( 𝜑 → ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐸 𝑌 ) )
17 16 eleq2d ( 𝜑 → ( 𝐹 ∈ ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ↔ 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ) )
18 2 8 oppchom ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐻 𝑌 )
19 18 a1i ( 𝜑 → ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐻 𝑌 ) )
20 19 eleq2d ( 𝜑 → ( 𝐹 ∈ ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ↔ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) )
21 2 8 oppchom ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) = ( 𝑌 𝐻 𝑧 )
22 21 a1i ( ( 𝜑𝑧𝐵 ) → ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) = ( 𝑌 𝐻 𝑧 ) )
23 simpr ( ( 𝜑𝑧𝐵 ) → 𝑧𝐵 )
24 7 adantr ( ( 𝜑𝑧𝐵 ) → 𝑌𝐵 )
25 6 adantr ( ( 𝜑𝑧𝐵 ) → 𝑋𝐵 )
26 1 3 8 23 24 25 oppcco ( ( 𝜑𝑧𝐵 ) → ( 𝐹 ( ⟨ 𝑧 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) = ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑧 ) 𝐹 ) )
27 22 26 mpteq12dv ( ( 𝜑𝑧𝐵 ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑧 ) 𝐹 ) ) )
28 27 cnveqd ( ( 𝜑𝑧𝐵 ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑧 ) 𝐹 ) ) )
29 28 funeqd ( ( 𝜑𝑧𝐵 ) → ( Fun ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) ↔ Fun ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑧 ) 𝐹 ) ) ) )
30 29 ralbidva ( 𝜑 → ( ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) ↔ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑧 ) 𝐹 ) ) ) )
31 20 30 anbi12d ( 𝜑 → ( ( 𝐹 ∈ ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) ∧ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑧 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) ↦ ( 𝐹 ( ⟨ 𝑧 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝑔 ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑧 ) 𝐹 ) ) ) ) )
32 15 17 31 3bitr3d ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧𝐵 Fun ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌· 𝑧 ) 𝐹 ) ) ) ) )