Metamath Proof Explorer

Theorem oppchofcl

Description: Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses oppchofcl.o ⊢ O = oppCat ⁡ C
oppchofcl.m ⊢ M = Hom F ⁡ O
oppchofcl.d ⊢ D = SetCat ⁡ U
oppchofcl.c ⊢ φ → C ∈ Cat
oppchofcl.u ⊢ φ → U ∈ V
oppchofcl.h ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ U
Assertion oppchofcl ⊢ φ → M ∈ C × c O Func D

Proof

Step Hyp Ref Expression
1 oppchofcl.o ⊢ O = oppCat ⁡ C
2 oppchofcl.m ⊢ M = Hom F ⁡ O
3 oppchofcl.d ⊢ D = SetCat ⁡ U
4 oppchofcl.c ⊢ φ → C ∈ Cat
5 oppchofcl.u ⊢ φ → U ∈ V
6 oppchofcl.h ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ U
7 eqid ⊢ oppCat ⁡ O = oppCat ⁡ O
8 1 oppccat ⊢ C ∈ Cat → O ∈ Cat
9 4 8 syl ⊢ φ → O ∈ Cat
10 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
11 1 10 oppchomf ⊢ tpos Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ O
12 11 rneqi ⊢ ran ⁡ tpos Hom 𝑓 ⁡ C = ran ⁡ Hom 𝑓 ⁡ O
13 relxp ⊢ Rel ⁡ Base C × Base C
14 eqid ⊢ Base C = Base C
15 10 14 homffn ⊢ Hom 𝑓 ⁡ C Fn Base C × Base C
16 15 fndmi ⊢ dom ⁡ Hom 𝑓 ⁡ C = Base C × Base C
17 16 releqi ⊢ Rel ⁡ dom ⁡ Hom 𝑓 ⁡ C ↔ Rel ⁡ Base C × Base C
18 13 17 mpbir ⊢ Rel ⁡ dom ⁡ Hom 𝑓 ⁡ C
19 rntpos ⊢ Rel ⁡ dom ⁡ Hom 𝑓 ⁡ C → ran ⁡ tpos Hom 𝑓 ⁡ C = ran ⁡ Hom 𝑓 ⁡ C
20 18 19 ax-mp ⊢ ran ⁡ tpos Hom 𝑓 ⁡ C = ran ⁡ Hom 𝑓 ⁡ C
21 12 20 eqtr3i ⊢ ran ⁡ Hom 𝑓 ⁡ O = ran ⁡ Hom 𝑓 ⁡ C
22 21 6 eqsstrid ⊢ φ → ran ⁡ Hom 𝑓 ⁡ O ⊆ U
23 2 7 3 9 5 22 hofcl ⊢ φ → M ∈ oppCat ⁡ O × c O Func D
24 1 2oppchomf ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
25 24 a1i ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
26 1 2oppccomf ⊢ comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
27 26 a1i ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
28 eqidd ⊢ φ → Hom 𝑓 ⁡ O = Hom 𝑓 ⁡ O
29 eqidd ⊢ φ → comp 𝑓 ⁡ O = comp 𝑓 ⁡ O
30 7 oppccat ⊢ O ∈ Cat → oppCat ⁡ O ∈ Cat
31 9 30 syl ⊢ φ → oppCat ⁡ O ∈ Cat
32 25 27 28 29 4 31 9 9 xpcpropd ⊢ φ → C × c O = oppCat ⁡ O × c O
33 32 oveq1d ⊢ φ → C × c O Func D = oppCat ⁡ O × c O Func D
34 23 33 eleqtrrd ⊢ φ → M ∈ C × c O Func D