Theorem oppff1

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

	Ref	Expression
Hypotheses	oppff1.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppff1.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
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=\mathrm{oppCat}\left(C\right)$$
2		oppff1.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		oppffn	Could not format oppFunc Fn ( _V X. _V ) : No typesetting found for |- oppFunc Fn ( _V X. _V ) with typecode |-
4		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
5		df-rel	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)\leftrightarrow C\mathrm{Func}D\subseteq \mathrm{V}\times \mathrm{V}$$
6	4 5	mpbi	$$⊢C\mathrm{Func}D\subseteq \mathrm{V}\times \mathrm{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 \left(C\mathrm{Func}D\right)\to f\in \left(C\mathrm{Func}D\right)$$
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	$$⊢\left(f\in \left(C\mathrm{Func}D\right)\wedge g\in \left(C\mathrm{Func}D\right)\right)\to f\in \left(C\mathrm{Func}D\right)$$
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	$$⊢\left(f\in \left(C\mathrm{Func}D\right)\wedge g\in \left(C\mathrm{Func}D\right)\right)\to g\in \left(C\mathrm{Func}D\right)$$
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	$$⊢\mathrm{Rel}\left(O\mathrm{Func}P\right)$$
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 |-