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 ◡ ( 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑧 ) 𝐹 ) ) ) ) )