Metamath Proof Explorer

Theorem fthepi

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

Ref Expression
Hypotheses fthmon.b ⊢ B = Base C
fthmon.h ⊢ H = Hom ⁡ C
fthmon.f ⊢ φ → F C Faith D G
fthmon.x ⊢ φ → X ∈ B
fthmon.y ⊢ φ → Y ∈ B
fthmon.r ⊢ φ → R ∈ X H Y
fthepi.e ⊢ E = Epi ⁡ C
fthepi.p ⊢ P = Epi ⁡ D
fthepi.1 ⊢ φ → X G Y ⁡ R ∈ F ⁡ X P F ⁡ Y
Assertion fthepi ⊢ φ → R ∈ X E Y

Proof

Step Hyp Ref Expression
1 fthmon.b ⊢ B = Base C
2 fthmon.h ⊢ H = Hom ⁡ C
3 fthmon.f ⊢ φ → F C Faith D G
4 fthmon.x ⊢ φ → X ∈ B
5 fthmon.y ⊢ φ → Y ∈ B
6 fthmon.r ⊢ φ → R ∈ X H Y
7 fthepi.e ⊢ E = Epi ⁡ C
8 fthepi.p ⊢ P = Epi ⁡ D
9 fthepi.1 ⊢ φ → X G Y ⁡ R ∈ F ⁡ X P F ⁡ Y
10 eqid ⊢ oppCat ⁡ C = oppCat ⁡ C
11 10 1 oppcbas ⊢ B = Base oppCat ⁡ C
12 eqid ⊢ Hom ⁡ oppCat ⁡ C = Hom ⁡ oppCat ⁡ C
13 eqid ⊢ oppCat ⁡ D = oppCat ⁡ D
14 10 13 3 fthoppc ⊢ φ → F oppCat ⁡ C Faith oppCat ⁡ D tpos G
15 2 10 oppchom ⊢ Y Hom ⁡ oppCat ⁡ C X = X H Y
16 6 15 eleqtrrdi ⊢ φ → R ∈ Y Hom ⁡ oppCat ⁡ C X
17 eqid ⊢ Mono ⁡ oppCat ⁡ C = Mono ⁡ oppCat ⁡ C
18 eqid ⊢ Mono ⁡ oppCat ⁡ D = Mono ⁡ oppCat ⁡ D
19 ovtpos ⊢ Y tpos G X = X G Y
20 19 fveq1i ⊢ Y tpos G X ⁡ R = X G Y ⁡ R
21 20 9 eqeltrid ⊢ φ → Y tpos G X ⁡ R ∈ F ⁡ X P F ⁡ Y
22 fthfunc ⊢ C Faith D ⊆ C Func D
23 22 ssbri ⊢ F C Faith D G → F C Func D G
24 3 23 syl ⊢ φ → F C Func D G
25 df-br ⊢ F C Func D G ↔ F G ∈ C Func D
26 24 25 sylib ⊢ φ → F G ∈ C Func D
27 funcrcl ⊢ F G ∈ C Func D → C ∈ Cat ∧ D ∈ Cat
28 26 27 syl ⊢ φ → C ∈ Cat ∧ D ∈ Cat
29 28 simprd ⊢ φ → D ∈ Cat
30 13 29 18 8 oppcmon ⊢ φ → F ⁡ Y Mono ⁡ oppCat ⁡ D F ⁡ X = F ⁡ X P F ⁡ Y
31 21 30 eleqtrrd ⊢ φ → Y tpos G X ⁡ R ∈ F ⁡ Y Mono ⁡ oppCat ⁡ D F ⁡ X
32 11 12 14 5 4 16 17 18 31 fthmon ⊢ φ → R ∈ Y Mono ⁡ oppCat ⁡ C X
33 28 simpld ⊢ φ → C ∈ Cat
34 10 33 17 7 oppcmon ⊢ φ → Y Mono ⁡ oppCat ⁡ C X = X E Y
35 32 34 eleqtrd ⊢ φ → R ∈ X E Y