oppff1

Description: The operation generating opposite functors is injective. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	oppff1.o	$⊢ O = oppCat (C)$
	oppff1.p	$⊢ P = oppCat (D)$
Assertion	oppff1	Could not format assertion : No typesetting found for \|- ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		oppff1.o	$⊢ O = oppCat (C)$
2		oppff1.p	$⊢ P = oppCat (D)$
3		oppffn	Could not format oppFunc Fn ( _V X. _V ) : No typesetting found for \|- oppFunc Fn ( _V X. _V ) with typecode \|-
4		relfunc	$⊢ Rel (C Func D)$
5		df-rel	$⊢ Rel (C Func D) \leftrightarrow C Func D \subseteq V \times V$
6	4 5	mpbi	$⊢ C Func D \subseteq V \times V$
7		fnssres	Could not format ( ( oppFunc Fn ( _V X. _V ) /\ ( C Func D ) C_ ( _V X. _V ) ) -> ( oppFunc \|` ( C Func D ) ) Fn ( C Func D ) ) : No typesetting found for \|- ( ( oppFunc Fn ( _V X. _V ) /\ ( C Func D ) C_ ( _V X. _V ) ) -> ( oppFunc \|` ( C Func D ) ) Fn ( C Func D ) ) with typecode \|-
8	3 6 7	mp2an	Could not format ( oppFunc \|` ( C Func D ) ) Fn ( C Func D ) : No typesetting found for \|- ( oppFunc \|` ( C Func D ) ) Fn ( C Func D ) with typecode \|-
9		fvres	Could not format ( f e. ( C Func D ) -> ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( oppFunc ` f ) ) : No typesetting found for \|- ( f e. ( C Func D ) -> ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( oppFunc ` f ) ) with typecode \|-
10		id	$⊢ f \in (C Func D) \to f \in (C Func D)$
11	1 2 10	oppfoppc2	Could not format ( f e. ( C Func D ) -> ( oppFunc ` f ) e. ( O Func P ) ) : No typesetting found for \|- ( f e. ( C Func D ) -> ( oppFunc ` f ) e. ( O Func P ) ) with typecode \|-
12	9 11	eqeltrd	Could not format ( f e. ( C Func D ) -> ( ( oppFunc \|` ( C Func D ) ) ` f ) e. ( O Func P ) ) : No typesetting found for \|- ( f e. ( C Func D ) -> ( ( oppFunc \|` ( C Func D ) ) ` f ) e. ( O Func P ) ) with typecode \|-
13	12	rgen	Could not format A. f e. ( C Func D ) ( ( oppFunc \|` ( C Func D ) ) ` f ) e. ( O Func P ) : No typesetting found for \|- A. f e. ( C Func D ) ( ( oppFunc \|` ( C Func D ) ) ` f ) e. ( O Func P ) with typecode \|-
14		ffnfv	Could not format ( ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) <-> ( ( oppFunc \|` ( C Func D ) ) Fn ( C Func D ) /\ A. f e. ( C Func D ) ( ( oppFunc \|` ( C Func D ) ) ` f ) e. ( O Func P ) ) ) : No typesetting found for \|- ( ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) <-> ( ( oppFunc \|` ( C Func D ) ) Fn ( C Func D ) /\ A. f e. ( C Func D ) ( ( oppFunc \|` ( C Func D ) ) ` f ) e. ( O Func P ) ) ) with typecode \|-
15	8 13 14	mpbir2an	Could not format ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) : No typesetting found for \|- ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) with typecode \|-
16		simpl	$⊢ (f \in (C Func D) \land g \in (C Func D)) \to f \in (C Func D)$
17	16	fvresd	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( oppFunc ` f ) ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( oppFunc ` f ) ) with typecode \|-
18		simpr	$⊢ (f \in (C Func D) \land g \in (C Func D)) \to g \in (C Func D)$
19	18	fvresd	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc \|` ( C Func D ) ) ` g ) = ( oppFunc ` g ) ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc \|` ( C Func D ) ) ` g ) = ( oppFunc ` g ) ) with typecode \|-
20	17 19	eqeq12d	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( ( oppFunc \|` ( C Func D ) ) ` g ) <-> ( oppFunc ` f ) = ( oppFunc ` g ) ) ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( ( oppFunc \|` ( C Func D ) ) ` g ) <-> ( oppFunc ` f ) = ( oppFunc ` g ) ) ) with typecode \|-
21		fveq2	Could not format ( ( oppFunc ` f ) = ( oppFunc ` g ) -> ( oppFunc ` ( oppFunc ` f ) ) = ( oppFunc ` ( oppFunc ` g ) ) ) : No typesetting found for \|- ( ( oppFunc ` f ) = ( oppFunc ` g ) -> ( oppFunc ` ( oppFunc ` f ) ) = ( oppFunc ` ( oppFunc ` g ) ) ) with typecode \|-
22	1 2 16	oppfoppc2	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` f ) e. ( O Func P ) ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` f ) e. ( O Func P ) ) with typecode \|-
23		relfunc	$⊢ Rel (O Func P)$
24		eqid	Could not format ( oppFunc ` f ) = ( oppFunc ` f ) : No typesetting found for \|- ( oppFunc ` f ) = ( oppFunc ` f ) with typecode \|-
25	22 23 24	2oppf	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` ( oppFunc ` f ) ) = f ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` ( oppFunc ` f ) ) = f ) with typecode \|-
26	1 2 18	oppfoppc2	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` g ) e. ( O Func P ) ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` g ) e. ( O Func P ) ) with typecode \|-
27		eqid	Could not format ( oppFunc ` g ) = ( oppFunc ` g ) : No typesetting found for \|- ( oppFunc ` g ) = ( oppFunc ` g ) with typecode \|-
28	26 23 27	2oppf	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` ( oppFunc ` g ) ) = g ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( oppFunc ` ( oppFunc ` g ) ) = g ) with typecode \|-
29	25 28	eqeq12d	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc ` ( oppFunc ` f ) ) = ( oppFunc ` ( oppFunc ` g ) ) <-> f = g ) ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc ` ( oppFunc ` f ) ) = ( oppFunc ` ( oppFunc ` g ) ) <-> f = g ) ) with typecode \|-
30	21 29	imbitrid	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc ` f ) = ( oppFunc ` g ) -> f = g ) ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( oppFunc ` f ) = ( oppFunc ` g ) -> f = g ) ) with typecode \|-
31	20 30	sylbid	Could not format ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( ( oppFunc \|` ( C Func D ) ) ` g ) -> f = g ) ) : No typesetting found for \|- ( ( f e. ( C Func D ) /\ g e. ( C Func D ) ) -> ( ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( ( oppFunc \|` ( C Func D ) ) ` g ) -> f = g ) ) with typecode \|-
32	31	rgen2	Could not format A. f e. ( C Func D ) A. g e. ( C Func D ) ( ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( ( oppFunc \|` ( C Func D ) ) ` g ) -> f = g ) : No typesetting found for \|- A. f e. ( C Func D ) A. g e. ( C Func D ) ( ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( ( oppFunc \|` ( C Func D ) ) ` g ) -> f = g ) with typecode \|-
33		dff13	Could not format ( ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) <-> ( ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) /\ A. f e. ( C Func D ) A. g e. ( C Func D ) ( ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( ( oppFunc \|` ( C Func D ) ) ` g ) -> f = g ) ) ) : No typesetting found for \|- ( ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) <-> ( ( oppFunc \|` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) /\ A. f e. ( C Func D ) A. g e. ( C Func D ) ( ( ( oppFunc \|` ( C Func D ) ) ` f ) = ( ( oppFunc \|` ( C Func D ) ) ` g ) -> f = g ) ) ) with typecode \|-
34	15 32 33	mpbir2an	Could not format ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) : No typesetting found for \|- ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) with typecode \|-

Metamath Proof Explorer

Theorem oppff1

Proof