Metamath Proof Explorer

Theorem oppchofcl

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

Ref Expression
Hypotheses oppchofcl.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppchofcl.m ⊢ 𝑀 = ( HomF ‘ 𝑂 )
oppchofcl.d ⊢ 𝐷 = ( SetCat ‘ 𝑈 )
oppchofcl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
oppchofcl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
oppchofcl.h ⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
Assertion oppchofcl ( 𝜑 → 𝑀 ∈ ( ( 𝐶 ×c 𝑂 ) Func 𝐷 ) )

Proof

Step Hyp Ref Expression
1 oppchofcl.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppchofcl.m ⊢ 𝑀 = ( HomF ‘ 𝑂 )
3 oppchofcl.d ⊢ 𝐷 = ( SetCat ‘ 𝑈 )
4 oppchofcl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 oppchofcl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6 oppchofcl.h ⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
7 eqid ⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
8 1 oppccat ⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
9 4 8 syl ⊢ ( 𝜑 → 𝑂 ∈ Cat )
10 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
11 1 10 oppchomf ⊢ tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 )
12 11 rneqi ⊢ ran tpos ( Homf ‘ 𝐶 ) = ran ( Homf ‘ 𝑂 )
13 relxp ⊢ Rel ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
14 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
15 10 14 homffn ⊢ ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
16 15 fndmi ⊢ dom ( Homf ‘ 𝐶 ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
17 16 releqi ⊢ ( Rel dom ( Homf ‘ 𝐶 ) ↔ Rel ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
18 13 17 mpbir ⊢ Rel dom ( Homf ‘ 𝐶 )
19 rntpos ⊢ ( Rel dom ( Homf ‘ 𝐶 ) → ran tpos ( Homf ‘ 𝐶 ) = ran ( Homf ‘ 𝐶 ) )
20 18 19 ax-mp ⊢ ran tpos ( Homf ‘ 𝐶 ) = ran ( Homf ‘ 𝐶 )
21 12 20 eqtr3i ⊢ ran ( Homf ‘ 𝑂 ) = ran ( Homf ‘ 𝐶 )
22 21 6 eqsstrid ⊢ ( 𝜑 → ran ( Homf ‘ 𝑂 ) ⊆ 𝑈 )
23 2 7 3 9 5 22 hofcl ⊢ ( 𝜑 → 𝑀 ∈ ( ( ( oppCat ‘ 𝑂 ) ×c 𝑂 ) Func 𝐷 ) )
24 1 2oppchomf ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
25 24 a1i ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
26 1 2oppccomf ⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
27 26 a1i ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
28 eqidd ⊢ ( 𝜑 → ( Homf ‘ 𝑂 ) = ( Homf ‘ 𝑂 ) )
29 eqidd ⊢ ( 𝜑 → ( compf ‘ 𝑂 ) = ( compf ‘ 𝑂 ) )
30 7 oppccat ⊢ ( 𝑂 ∈ Cat → ( oppCat ‘ 𝑂 ) ∈ Cat )
31 9 30 syl ⊢ ( 𝜑 → ( oppCat ‘ 𝑂 ) ∈ Cat )
32 25 27 28 29 4 31 9 9 xpcpropd ⊢ ( 𝜑 → ( 𝐶 ×c 𝑂 ) = ( ( oppCat ‘ 𝑂 ) ×c 𝑂 ) )
33 32 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 ×c 𝑂 ) Func 𝐷 ) = ( ( ( oppCat ‘ 𝑂 ) ×c 𝑂 ) Func 𝐷 ) )
34 23 33 eleqtrrd ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝐶 ×c 𝑂 ) Func 𝐷 ) )