2oppffunc

Description: The opposite functor of an opposite functor is a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025) The functor in opposite categories does not have to be an opposite functor. (Revised by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	funcoppc2.o	$⊢ O = oppCat (C)$
	funcoppc2.p	$⊢ P = oppCat (D)$
	funcoppc2.c	$⊢ φ \to C \in V$
	funcoppc2.d	$⊢ φ \to D \in W$
	2oppffunc.f	$⊢ φ \to F \in (O Func P)$
Assertion	2oppffunc	Could not format assertion : No typesetting found for \|- ( ph -> ( oppFunc ` F ) e. ( C Func D ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		funcoppc2.o	$⊢ O = oppCat (C)$
2		funcoppc2.p	$⊢ P = oppCat (D)$
3		funcoppc2.c	$⊢ φ \to C \in V$
4		funcoppc2.d	$⊢ φ \to D \in W$
5		2oppffunc.f	$⊢ φ \to F \in (O Func P)$
6		oppfval2	Could not format ( F e. ( O Func P ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for \|- ( F e. ( O Func P ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-
7	5 6	syl	Could not format ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for \|- ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-
8	5	func1st2nd	$⊢ φ \to 1^{st} (F) (O Func P) 2^{nd} (F)$
9	1 2 3 4 8	funcoppc2	$⊢ φ \to 1^{st} (F) (C Func D) tpos 2^{nd} (F)$
10		df-br	$⊢ 1^{st} (F) (C Func D) tpos 2^{nd} (F) \leftrightarrow ⟨1^{st} (F), tpos 2^{nd} (F)⟩ \in (C Func D)$
11	9 10	sylib	$⊢ φ \to ⟨1^{st} (F), tpos 2^{nd} (F)⟩ \in (C Func D)$
12	7 11	eqeltrd	Could not format ( ph -> ( oppFunc ` F ) e. ( C Func D ) ) : No typesetting found for \|- ( ph -> ( oppFunc ` F ) e. ( C Func D ) ) with typecode \|-

Metamath Proof Explorer

Theorem 2oppffunc

Proof