oppfoppc2

Description: The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 14-Nov-2025)

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

Step	Hyp	Ref	Expression
1		oppfoppc.o	$⊢ O = oppCat (C)$
2		oppfoppc.p	$⊢ P = oppCat (D)$
3		oppfoppc2.f	$⊢ φ \to F \in (C Func D)$
4		relfunc	$⊢ Rel (C Func D)$
5		1st2nd	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
6	4 3 5	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
7	6	fveq2d	Could not format ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for \|- ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode \|-
8		df-ov	Could not format ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) : No typesetting found for \|- ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) with typecode \|-
9	7 8	eqtr4di	Could not format ( ph -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) ) : No typesetting found for \|- ( ph -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) ) with typecode \|-
10	3	func1st2nd	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
11	1 2 10	oppfoppc	Could not format ( ph -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) e. ( O Func P ) ) : No typesetting found for \|- ( ph -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) e. ( O Func P ) ) with typecode \|-
12	9 11	eqeltrd	Could not format ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) : No typesetting found for \|- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode \|-

Metamath Proof Explorer