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

Metamath Proof Explorer

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

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		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	$⊢ Rel (O Func P)$
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	$⊢ φ \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	$⊢ φ \to (Rel G \land Rel dom G)$
16		tpostpos2	$⊢ (Rel G \land Rel dom G) \to tpos tpos G = G$
17	15 16	syl	$⊢ φ \to tpos tpos G = 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	$⊢ φ \to F (C Func D) G$