Theorem funcoppc4

Description: A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	funcoppc2.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	funcoppc2.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	funcoppc2.c	$$⊢\phi \to C\in V$$
	funcoppc2.d	$$⊢\phi \to D\in W$$
	funcoppc4.f	No typesetting found for |- ( ph -> ( F oppFunc G ) e. ( O Func P ) ) with typecode |-
Assertion	funcoppc4	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$

Proof

Step	Hyp	Ref	Expression
1		funcoppc2.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		funcoppc2.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		funcoppc2.c	$$⊢\phi \to C\in V$$
4		funcoppc2.d	$$⊢\phi \to D\in W$$
5		funcoppc4.f	Could not format ( ph -> ( F oppFunc G ) e. ( O Func P ) ) : No typesetting found for |- ( ph -> ( F oppFunc G ) e. ( O Func P ) ) with typecode |-
6	5	func1st2nd	Could not format ( ph -> ( 1st ` ( F oppFunc G ) ) ( O Func P ) ( 2nd ` ( F oppFunc G ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( F oppFunc G ) ) ( O Func P ) ( 2nd ` ( F oppFunc G ) ) ) with typecode |-
7	1 2 3 4 6	funcoppc2	Could not format ( ph -> ( 1st ` ( F oppFunc G ) ) ( C Func D ) tpos ( 2nd ` ( F oppFunc G ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( F oppFunc G ) ) ( C Func D ) tpos ( 2nd ` ( F oppFunc G ) ) ) with typecode |-
8		relfunc	$$⊢\mathrm{Rel}\left(O\mathrm{Func}P\right)$$
9		df-ov	Could not format ( F oppFunc G ) = ( oppFunc ` <. F , G >. ) : No typesetting found for |- ( F oppFunc G ) = ( oppFunc ` <. F , G >. ) with typecode |-
10		eqidd	$$⊢\phi \to ⟨F,G⟩=⟨F,G⟩$$
11	5 8 9 10	oppf1st2nd	Could not format ( ph -> ( ( F oppFunc G ) e. ( _V X. _V ) /\ ( ( 1st ` ( F oppFunc G ) ) = F /\ ( 2nd ` ( F oppFunc G ) ) = tpos G ) ) ) : No typesetting found for |- ( ph -> ( ( F oppFunc G ) e. ( _V X. _V ) /\ ( ( 1st ` ( F oppFunc G ) ) = F /\ ( 2nd ` ( F oppFunc G ) ) = tpos G ) ) ) with typecode |-
12	11	simprld	Could not format ( ph -> ( 1st ` ( F oppFunc G ) ) = F ) : No typesetting found for |- ( ph -> ( 1st ` ( F oppFunc G ) ) = F ) with typecode |-
13	11	simprrd	Could not format ( ph -> ( 2nd ` ( F oppFunc G ) ) = tpos G ) : No typesetting found for |- ( ph -> ( 2nd ` ( F oppFunc G ) ) = tpos G ) with typecode |-
14	13	tposeqd	Could not format ( ph -> tpos ( 2nd ` ( F oppFunc G ) ) = tpos tpos G ) : No typesetting found for |- ( ph -> tpos ( 2nd ` ( F oppFunc G ) ) = tpos tpos G ) with typecode |-
15	5 8 9 10	oppfrcl3	$$⊢\phi \to \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)$$
16		tpostpos2	$$⊢\left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)\to tpostposG=G$$
17	15 16	syl	$$⊢\phi \to tpostposG=G$$
18	14 17	eqtrd	Could not format ( ph -> tpos ( 2nd ` ( F oppFunc G ) ) = G ) : No typesetting found for |- ( ph -> tpos ( 2nd ` ( F oppFunc G ) ) = G ) with typecode |-
19	7 12 18	3brtr3d	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$