Theorem fucoppclem

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

	Ref	Expression
Hypotheses	fucoppclem.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	fucoppclem.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	fucoppclem.n	$$⊢N=C\mathrm{Nat}D$$
	fucoppclem.f	No typesetting found for |- ( ph -> F = ( oppFunc |` ( C Func D ) ) ) with typecode |-
	fucoppclem.x	$$⊢\phi \to X\in \left(C\mathrm{Func}D\right)$$
	fucoppclem.y	$$⊢\phi \to Y\in \left(C\mathrm{Func}D\right)$$
Assertion	fucoppclem	$$⊢\phi \to YNX=F\left(X\right)\left(O\mathrm{Nat}P\right)F\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		fucoppclem.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		fucoppclem.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		fucoppclem.n	$$⊢N=C\mathrm{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	$$⊢\phi \to X\in \left(C\mathrm{Func}D\right)$$
6		fucoppclem.y	$$⊢\phi \to Y\in \left(C\mathrm{Func}D\right)$$
7		eqid	$$⊢O\mathrm{Nat}P=O\mathrm{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	$$⊢\phi \to 1^{st}\left(X\right)\left(C\mathrm{Func}D\right)2^{nd}\left(X\right)$$
15	14	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
16	14	funcrcl3	$$⊢\phi \to D\in \mathrm{Cat}$$
17	1 2 3 7 10 13 15 16	natoppfb	$$⊢\phi \to YNX=F\left(X\right)\left(O\mathrm{Nat}P\right)F\left(Y\right)$$