Metamath Proof Explorer

Theorem oppcmon

Description: A monomorphism in the opposite category is an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses oppcmon.o ⊢ O = oppCat ⁡ C
oppcmon.c ⊢ φ → C ∈ Cat
oppcmon.m ⊢ M = Mono ⁡ O
oppcmon.e ⊢ E = Epi ⁡ C
Assertion oppcmon ⊢ φ → X M Y = Y E X

Proof

Step Hyp Ref Expression
1 oppcmon.o ⊢ O = oppCat ⁡ C
2 oppcmon.c ⊢ φ → C ∈ Cat
3 oppcmon.m ⊢ M = Mono ⁡ O
4 oppcmon.e ⊢ E = Epi ⁡ C
5 fveq2 ⊢ c = C → oppCat ⁡ c = oppCat ⁡ C
6 5 1 eqtr4di ⊢ c = C → oppCat ⁡ c = O
7 6 fveq2d ⊢ c = C → Mono ⁡ oppCat ⁡ c = Mono ⁡ O
8 7 3 eqtr4di ⊢ c = C → Mono ⁡ oppCat ⁡ c = M
9 8 tposeqd ⊢ c = C → tpos Mono ⁡ oppCat ⁡ c = tpos M
10 df-epi ⊢ Epi = c ∈ Cat ⟼ tpos Mono ⁡ oppCat ⁡ c
11 3 fvexi ⊢ M ∈ V
12 11 tposex ⊢ tpos M ∈ V
13 9 10 12 fvmpt ⊢ C ∈ Cat → Epi ⁡ C = tpos M
14 2 13 syl ⊢ φ → Epi ⁡ C = tpos M
15 4 14 eqtrid ⊢ φ → E = tpos M
16 15 oveqd ⊢ φ → Y E X = Y tpos M X
17 ovtpos ⊢ Y tpos M X = X M Y
18 16 17 eqtr2di ⊢ φ → X M Y = Y E X