oppfval

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

		Ref	Expression
	Assertion	oppfval	Could not format assertion : No typesetting found for \|- ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. ) with typecode \|-

Step	Hyp	Ref	Expression
1		relfunc	$⊢ Rel (C Func D)$
2	1	brrelex12i	$⊢ F (C Func D) G \to (F \in V \land G \in V)$
3		oppfvalg	Could not format ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) : No typesetting found for \|- ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) with typecode \|-
4	2 3	syl	Could not format ( F ( C Func D ) G -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) : No typesetting found for \|- ( F ( C Func D ) G -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) with typecode \|-
5		oppfvallem	$⊢ F (C Func D) G \to (Rel G \land Rel dom G)$
6	5	iftrued	$⊢ F (C Func D) G \to if ((Rel G \land Rel dom G), ⟨F, tpos G⟩, \emptyset) = ⟨F, tpos G⟩$
7	4 6	eqtrd	Could not format ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. ) : No typesetting found for \|- ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. ) with typecode \|-

Metamath Proof Explorer