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 𝑃 ) ( 𝐹 ‘ 𝑌 ) ) )