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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
fucoppclem.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
fucoppclem.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
fucoppclem.f ⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
fucoppclem.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐷 ) )
fucoppclem.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝐷 ) )
Assertion fucoppclem ( 𝜑 → ( 𝑌 𝑁 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 fucoppclem.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 fucoppclem.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 fucoppclem.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
4 fucoppclem.f ⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
5 fucoppclem.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐷 ) )
6 fucoppclem.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝐷 ) )
7 eqid ⊢ ( 𝑂 Nat 𝑃 ) = ( 𝑂 Nat 𝑃 )
8 4 fveq1d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑌 ) )
9 6 fvresd ⊢ ( 𝜑 → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑌 ) = ( oppFunc ‘ 𝑌 ) )
10 8 9 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = ( oppFunc ‘ 𝑌 ) )
11 4 fveq1d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑋 ) )
12 5 fvresd ⊢ ( 𝜑 → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑋 ) = ( oppFunc ‘ 𝑋 ) )
13 11 12 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( oppFunc ‘ 𝑋 ) )
14 5 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝑋 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝑋 ) )
15 14 funcrcl2 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
16 14 funcrcl3 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
17 1 2 3 7 10 13 15 16 natoppfb ⊢ ( 𝜑 → ( 𝑌 𝑁 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑌 ) ) )