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

Metamath Proof Explorer

Theorem oppfuprcl

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

Ref Expression
Hypotheses uprcl2a.x No typesetting found for |- ( ph -> X ( G ( O UP P ) W ) M ) with typecode |-
oppfuprcl.g No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
oppfuprcl.o ⊢ O = oppCat ⁡ D
oppfuprcl.p ⊢ P = oppCat ⁡ E
oppfuprcl.d ⊢ φ → D ∈ U
oppfuprcl.e ⊢ φ → E ∈ V
Assertion oppfuprcl ⊢ φ → F ∈ D Func E

Proof

Step Hyp Ref Expression
1 uprcl2a.x Could not format ( ph -> X ( G ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( G ( O UP P ) W ) M ) with typecode |-
2 oppfuprcl.g Could not format G = ( oppFunc ` F ) : No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
3 oppfuprcl.o ⊢ O = oppCat ⁡ D
4 oppfuprcl.p ⊢ P = oppCat ⁡ E
5 oppfuprcl.d ⊢ φ → D ∈ U
6 oppfuprcl.e ⊢ φ → E ∈ V
7 1 uprcl2a ⊢ φ → G ∈ O Func P
8 2 7 eqeltrrid Could not format ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode |-
9 3 4 5 6 8 funcoppc5 ⊢ φ → F ∈ D Func E