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

Metamath Proof Explorer

Theorem oppfuprcl2

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
oppfuprcl2.f ⊢ φ → F = A B
Assertion oppfuprcl2 ⊢ φ → A D Func E B

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 oppfuprcl2.f ⊢ φ → F = A B
8 1 2 3 4 5 6 oppfuprcl ⊢ φ → F ∈ D Func E
9 7 8 eqeltrrd ⊢ φ → A B ∈ D Func E
10 df-br ⊢ A D Func E B ↔ A B ∈ D Func E
11 9 10 sylibr ⊢ φ → A D Func E B