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

Metamath Proof Explorer

Theorem funcoppc5

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 ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
funcoppc5.f ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Func 𝑃 ) )
Assertion funcoppc5 ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )

Proof

Step Hyp Ref Expression
1 funcoppc2.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 funcoppc2.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 funcoppc2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 funcoppc2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5 funcoppc5.f ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Func 𝑃 ) )
6 relfunc ⊢ Rel ( 𝑂 Func 𝑃 )
7 eqid ⊢ ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ 𝐹 )
8 5 6 7 oppfrcl ⊢ ( 𝜑 → 𝐹 ∈ ( V × V ) )
9 1st2nd2 ⊢ ( 𝐹 ∈ ( V × V ) → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
10 8 9 syl ⊢ ( 𝜑 → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
11 10 fveq2d ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )
12 df-ov ⊢ ( ( 1st ‘ 𝐹 ) oppFunc ( 2nd ‘ 𝐹 ) ) = ( oppFunc ‘ ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
13 11 12 eqtr4di ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ( ( 1st ‘ 𝐹 ) oppFunc ( 2nd ‘ 𝐹 ) ) )
14 13 5 eqeltrrd ⊢ ( 𝜑 → ( ( 1st ‘ 𝐹 ) oppFunc ( 2nd ‘ 𝐹 ) ) ∈ ( 𝑂 Func 𝑃 ) )
15 1 2 3 4 14 funcoppc4 ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
16 df-br ⊢ ( ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) ↔ ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ∈ ( 𝐶 Func 𝐷 ) )
17 15 16 sylib ⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ∈ ( 𝐶 Func 𝐷 ) )
18 10 17 eqeltrd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )