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

Metamath Proof Explorer

Theorem fucoppclem

Description: Lemma for fucoppc . (Contributed by Zhi Wang, 18-Nov-2025)

Ref Expression
Hypotheses fucoppclem.o ⊢ O = oppCat ⁡ C
fucoppclem.p ⊢ P = oppCat ⁡ D
fucoppclem.n ⊢ N = C Nat D
fucoppclem.f No typesetting found for |- ( ph -> F = ( oppFunc |` ( C Func D ) ) ) with typecode |-
fucoppclem.x ⊢ φ → X ∈ C Func D
fucoppclem.y ⊢ φ → Y ∈ C Func D
Assertion fucoppclem ⊢ φ → Y N X = F ⁡ X O Nat P F ⁡ Y

Proof

Step Hyp Ref Expression
1 fucoppclem.o ⊢ O = oppCat ⁡ C
2 fucoppclem.p ⊢ P = oppCat ⁡ D
3 fucoppclem.n ⊢ N = C Nat D
4 fucoppclem.f Could not format ( ph -> F = ( oppFunc |` ( C Func D ) ) ) : No typesetting found for |- ( ph -> F = ( oppFunc |` ( C Func D ) ) ) with typecode |-
5 fucoppclem.x ⊢ φ → X ∈ C Func D
6 fucoppclem.y ⊢ φ → Y ∈ C Func D
7 eqid ⊢ O Nat P = O Nat P
8 4 fveq1d Could not format ( ph -> ( F ` Y ) = ( ( oppFunc |` ( C Func D ) ) ` Y ) ) : No typesetting found for |- ( ph -> ( F ` Y ) = ( ( oppFunc |` ( C Func D ) ) ` Y ) ) with typecode |-
9 6 fvresd Could not format ( ph -> ( ( oppFunc |` ( C Func D ) ) ` Y ) = ( oppFunc ` Y ) ) : No typesetting found for |- ( ph -> ( ( oppFunc |` ( C Func D ) ) ` Y ) = ( oppFunc ` Y ) ) with typecode |-
10 8 9 eqtrd Could not format ( ph -> ( F ` Y ) = ( oppFunc ` Y ) ) : No typesetting found for |- ( ph -> ( F ` Y ) = ( oppFunc ` Y ) ) with typecode |-
11 4 fveq1d Could not format ( ph -> ( F ` X ) = ( ( oppFunc |` ( C Func D ) ) ` X ) ) : No typesetting found for |- ( ph -> ( F ` X ) = ( ( oppFunc |` ( C Func D ) ) ` X ) ) with typecode |-
12 5 fvresd Could not format ( ph -> ( ( oppFunc |` ( C Func D ) ) ` X ) = ( oppFunc ` X ) ) : No typesetting found for |- ( ph -> ( ( oppFunc |` ( C Func D ) ) ` X ) = ( oppFunc ` X ) ) with typecode |-
13 11 12 eqtrd Could not format ( ph -> ( F ` X ) = ( oppFunc ` X ) ) : No typesetting found for |- ( ph -> ( F ` X ) = ( oppFunc ` X ) ) with typecode |-
14 5 func1st2nd ⊢ φ → 1 st ⁡ X C Func D 2 nd ⁡ X
15 14 funcrcl2 ⊢ φ → C ∈ Cat
16 14 funcrcl3 ⊢ φ → D ∈ Cat
17 1 2 3 7 10 13 15 16 natoppfb ⊢ φ → Y N X = F ⁡ X O Nat P F ⁡ Y