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	|- ( ph -> F = ( oppFunc |` ( C Func D ) ) )
	fucoppclem.x	|- ( ph -> X e. ( C Func D ) )
	fucoppclem.y	|- ( ph -> Y e. ( C Func D ) )
Assertion	fucoppclem	|- ( ph -> ( 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	|- ( ph -> F = ( oppFunc |` ( C Func D ) ) )
5		fucoppclem.x	|- ( ph -> X e. ( C Func D ) )
6		fucoppclem.y	|- ( ph -> Y e. ( C Func D ) )
7		eqid	|- ( O Nat P ) = ( O Nat P )
8	4	fveq1d	|- ( ph -> ( F ` Y ) = ( ( oppFunc |` ( C Func D ) ) ` Y ) )
9	6	fvresd	|- ( ph -> ( ( oppFunc |` ( C Func D ) ) ` Y ) = ( oppFunc ` Y ) )
10	8 9	eqtrd	|- ( ph -> ( F ` Y ) = ( oppFunc ` Y ) )
11	4	fveq1d	|- ( ph -> ( F ` X ) = ( ( oppFunc |` ( C Func D ) ) ` X ) )
12	5	fvresd	|- ( ph -> ( ( oppFunc |` ( C Func D ) ) ` X ) = ( oppFunc ` X ) )
13	11 12	eqtrd	|- ( ph -> ( F ` X ) = ( oppFunc ` X ) )
14	5	func1st2nd	|- ( ph -> ( 1st ` X ) ( C Func D ) ( 2nd ` X ) )
15	14	funcrcl2	|- ( ph -> C e. Cat )
16	14	funcrcl3	|- ( ph -> D e. Cat )
17	1 2 3 7 10 13 15 16	natoppfb	|- ( ph -> ( Y N X ) = ( ( F ` X ) ( O Nat P ) ( F ` Y ) ) )