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

Metamath Proof Explorer

Theorem oppcuprcl5

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
oppcuprcl5.j ⊢ J = Hom ⁡ E
Assertion oppcuprcl5 ⊢ φ → M ∈ F ⁡ X J W

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 oppcuprcl5.j ⊢ J = Hom ⁡ E
4 eqid ⊢ Hom ⁡ P = Hom ⁡ P
5 1 4 uprcl5 ⊢ φ → M ∈ W Hom ⁡ P F ⁡ X
6 3 2 oppchom ⊢ W Hom ⁡ P F ⁡ X = F ⁡ X J W
7 5 6 eleqtrdi ⊢ φ → M ∈ F ⁡ X J W