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

Metamath Proof Explorer

Theorem oppfval2

Description: Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025)

		Ref	Expression
	Assertion	oppfval2	Could not format assertion : No typesetting found for \|- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		relfunc	$⊢ Rel (C Func D)$
2		1st2nd	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
3	1 2	mpan	$⊢ F \in (C Func D) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
4	3	fveq2d	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for \|- ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode \|-
5		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 \|-
6	4 5	eqtr4di	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) ) : No typesetting found for \|- ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) ) with typecode \|-
7		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
8	1 7	mpan	$⊢ F \in (C Func D) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
9		oppfval	Could not format ( ( 1st ` F ) ( C Func D ) ( 2nd ` F ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for \|- ( ( 1st ` F ) ( C Func D ) ( 2nd ` F ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-
10	8 9	syl	Could not format ( F e. ( C Func D ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for \|- ( F e. ( C Func D ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-
11	6 10	eqtrd	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for \|- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-