This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcoppc5

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 = oppCat (C)$
		funcoppc2.p	$⊢ P = oppCat (D)$
		funcoppc2.c	$⊢ φ \to C \in V$
		funcoppc2.d	$⊢ φ \to D \in W$
		funcoppc5.f	No typesetting found for \|- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode \|-
	Assertion	funcoppc5	$⊢ φ \to F \in (C Func D)$

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		funcoppc5.f	Could not format ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) : No typesetting found for \|- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode \|-
6		relfunc	$⊢ Rel (O Func P)$
7		eqid	Could not format ( oppFunc ` F ) = ( oppFunc ` F ) : No typesetting found for \|- ( oppFunc ` F ) = ( oppFunc ` F ) with typecode \|-
8	5 6 7	oppfrcl	$⊢ φ \to F \in (V \times V)$
9		1st2nd2	$⊢ F \in (V \times V) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
10	8 9	syl	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
11	10	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 \|-
12		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 \|-
13	11 12	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 \|-
14	13 5	eqeltrrd	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 \|-
15	1 2 3 4 14	funcoppc4	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
16		df-br	$⊢ 1^{st} (F) (C Func D) 2^{nd} (F) \leftrightarrow ⟨1^{st} (F), 2^{nd} (F)⟩ \in (C Func D)$
17	15 16	sylib	$⊢ φ \to ⟨1^{st} (F), 2^{nd} (F)⟩ \in (C Func D)$
18	10 17	eqeltrd	$⊢ φ \to F \in (C Func D)$