This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcoppc4

Description: A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses funcoppc2.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
funcoppc2.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
funcoppc2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
funcoppc2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
funcoppc4.f ⊢ ( 𝜑 → ( 𝐹 oppFunc 𝐺 ) ∈ ( 𝑂 Func 𝑃 ) )
Assertion funcoppc4 ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 funcoppc2.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 funcoppc2.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 funcoppc2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 funcoppc2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5 funcoppc4.f ⊢ ( 𝜑 → ( 𝐹 oppFunc 𝐺 ) ∈ ( 𝑂 Func 𝑃 ) )
6 5 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 oppFunc 𝐺 ) ) ( 𝑂 Func 𝑃 ) ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) )
7 1 2 3 4 6 funcoppc2 ⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 oppFunc 𝐺 ) ) ( 𝐶 Func 𝐷 ) tpos ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) )
8 relfunc ⊢ Rel ( 𝑂 Func 𝑃 )
9 df-ov ⊢ ( 𝐹 oppFunc 𝐺 ) = ( oppFunc ‘ ⟨ 𝐹 , 𝐺 ⟩ )
10 eqidd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ⟨ 𝐹 , 𝐺 ⟩ )
11 5 8 9 10 oppf1st2nd ⊢ ( 𝜑 → ( ( 𝐹 oppFunc 𝐺 ) ∈ ( V × V ) ∧ ( ( 1st ‘ ( 𝐹 oppFunc 𝐺 ) ) = 𝐹 ∧ ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) = tpos 𝐺 ) ) )
12 11 simprld ⊢ ( 𝜑 → ( 1st ‘ ( 𝐹 oppFunc 𝐺 ) ) = 𝐹 )
13 11 simprrd ⊢ ( 𝜑 → ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) = tpos 𝐺 )
14 13 tposeqd ⊢ ( 𝜑 → tpos ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) = tpos tpos 𝐺 )
15 5 8 9 10 oppfrcl3 ⊢ ( 𝜑 → ( Rel 𝐺 ∧ Rel dom 𝐺 ) )
16 tpostpos2 ⊢ ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) → tpos tpos 𝐺 = 𝐺 )
17 15 16 syl ⊢ ( 𝜑 → tpos tpos 𝐺 = 𝐺 )
18 14 17 eqtrd ⊢ ( 𝜑 → tpos ( 2nd ‘ ( 𝐹 oppFunc 𝐺 ) ) = 𝐺 )
19 7 12 18 3brtr3d ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )