Metamath Proof Explorer

Theorem fthepi

Description: A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
fthmon.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
fthmon.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
fthmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
fthmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
fthmon.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
fthepi.e ⊢ 𝐸 = ( Epi ‘ 𝐶 )
fthepi.p ⊢ 𝑃 = ( Epi ‘ 𝐷 )
fthepi.1 ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝑃 ( 𝐹 ‘ 𝑌 ) ) )
Assertion fthepi ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐸 𝑌 ) )

Proof

Step Hyp Ref Expression
1 fthmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fthmon.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 fthmon.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
4 fthmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 fthmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 fthmon.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
7 fthepi.e ⊢ 𝐸 = ( Epi ‘ 𝐶 )
8 fthepi.p ⊢ 𝑃 = ( Epi ‘ 𝐷 )
9 fthepi.1 ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝑃 ( 𝐹 ‘ 𝑌 ) ) )
10 eqid ⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
11 10 1 oppcbas ⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) )
12 eqid ⊢ ( Hom ‘ ( oppCat ‘ 𝐶 ) ) = ( Hom ‘ ( oppCat ‘ 𝐶 ) )
13 eqid ⊢ ( oppCat ‘ 𝐷 ) = ( oppCat ‘ 𝐷 )
14 10 13 3 fthoppc ⊢ ( 𝜑 → 𝐹 ( ( oppCat ‘ 𝐶 ) Faith ( oppCat ‘ 𝐷 ) ) tpos 𝐺 )
15 2 10 oppchom ⊢ ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐻 𝑌 )
16 6 15 eleqtrrdi ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑌 ( Hom ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) )
17 eqid ⊢ ( Mono ‘ ( oppCat ‘ 𝐶 ) ) = ( Mono ‘ ( oppCat ‘ 𝐶 ) )
18 eqid ⊢ ( Mono ‘ ( oppCat ‘ 𝐷 ) ) = ( Mono ‘ ( oppCat ‘ 𝐷 ) )
19 ovtpos ⊢ ( 𝑌 tpos 𝐺 𝑋 ) = ( 𝑋 𝐺 𝑌 )
20 19 fveq1i ⊢ ( ( 𝑌 tpos 𝐺 𝑋 ) ‘ 𝑅 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 )
21 20 9 eqeltrid ⊢ ( 𝜑 → ( ( 𝑌 tpos 𝐺 𝑋 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝑃 ( 𝐹 ‘ 𝑌 ) ) )
22 fthfunc ⊢ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
23 22 ssbri ⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
24 3 23 syl ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
25 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
26 24 25 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
27 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
28 26 27 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
29 28 simprd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
30 13 29 18 8 oppcmon ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑌 ) ( Mono ‘ ( oppCat ‘ 𝐷 ) ) ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝑃 ( 𝐹 ‘ 𝑌 ) ) )
31 21 30 eleqtrrd ⊢ ( 𝜑 → ( ( 𝑌 tpos 𝐺 𝑋 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑌 ) ( Mono ‘ ( oppCat ‘ 𝐷 ) ) ( 𝐹 ‘ 𝑋 ) ) )
32 11 12 14 5 4 16 17 18 31 fthmon ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) )
33 28 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
34 10 33 17 7 oppcmon ⊢ ( 𝜑 → ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐸 𝑌 ) )
35 32 34 eleqtrd ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐸 𝑌 ) )