Metamath Proof Explorer

Theorem epii

Description: Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses isepi.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isepi.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
isepi.o ⊢ · = ( comp ‘ 𝐶 )
isepi.e ⊢ 𝐸 = ( Epi ‘ 𝐶 )
isepi.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
isepi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
isepi.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
epii.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
epii.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) )
epii.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
epii.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑌 𝐻 𝑍 ) )
Assertion epii ( 𝜑 → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ↔ 𝐺 = 𝐾 ) )

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 epii.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
9 epii.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐸 𝑌 ) )
10 epii.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
11 epii.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑌 𝐻 𝑍 ) )
12 eqid ⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
13 1 3 12 8 7 6 oppcco ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝐺 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
14 1 3 12 8 7 6 oppcco ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝐾 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
15 13 14 eqeq12d ⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝐾 ) ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) )
16 12 1 oppcbas ⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) )
17 eqid ⊢ ( Hom ‘ ( oppCat ‘ 𝐶 ) ) = ( Hom ‘ ( oppCat ‘ 𝐶 ) )
18 eqid ⊢ ( comp ‘ ( oppCat ‘ 𝐶 ) ) = ( comp ‘ ( oppCat ‘ 𝐶 ) )
19 eqid ⊢ ( Mono ‘ ( oppCat ‘ 𝐶 ) ) = ( Mono ‘ ( oppCat ‘ 𝐶 ) )
20 12 oppccat ⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat )
21 5 20 syl ⊢ ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat )
22 12 5 19 4 oppcmon ⊢ ( 𝜑 → ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐸 𝑌 ) )
23 9 22 eleqtrrd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) )
24 2 12 oppchom ⊢ ( 𝑍 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) = ( 𝑌 𝐻 𝑍 )
25 10 24 eleqtrrdi ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) )
26 11 24 eleqtrrdi ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) )
27 16 17 18 19 21 7 6 8 23 25 26 moni ⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝐺 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑌 ⟩ ( comp ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝐾 ) ↔ 𝐺 = 𝐾 ) )
28 15 27 bitr3d ⊢ ( 𝜑 → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ↔ 𝐺 = 𝐾 ) )