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

Metamath Proof Explorer

Theorem oppcuprcl2

Description: Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses oppcuprcl2.x No typesetting found for |- ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) with typecode |-
oppcuprcl2.p ⊢ P = oppCat ⁡ E
oppcuprcl2.o ⊢ O = oppCat ⁡ D
oppcuprcl2.d ⊢ φ → D ∈ U
oppcuprcl2.e ⊢ φ → E ∈ V
oppcuprcl2.h ⊢ φ → tpos G = H
Assertion oppcuprcl2 ⊢ φ → F D Func E H

Proof

Step Hyp Ref Expression
1 oppcuprcl2.x Could not format ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , G >. ( O UP P ) W ) M ) with typecode |-
2 oppcuprcl2.p ⊢ P = oppCat ⁡ E
3 oppcuprcl2.o ⊢ O = oppCat ⁡ D
4 oppcuprcl2.d ⊢ φ → D ∈ U
5 oppcuprcl2.e ⊢ φ → E ∈ V
6 oppcuprcl2.h ⊢ φ → tpos G = H
7 1 uprcl2 ⊢ φ → F O Func P G
8 3 2 4 5 7 funcoppc2 ⊢ φ → F D Func E tpos G
9 8 6 breqtrd ⊢ φ → F D Func E H