Theorem oppff1o

Description: The operation generating opposite functors is bijective. (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)$$
	oppff1o.c	$$⊢\phi \to C\in V$$
	oppff1o.d	$$⊢\phi \to D\in W$$
Assertion	oppff1o	Could not format assertion : No typesetting found for |- ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( 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		oppff1o.c	$$⊢\phi \to C\in V$$
4		oppff1o.d	$$⊢\phi \to D\in W$$
5	1 2	oppff1	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 |-
6	5	a1i	Could not format ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) ) : No typesetting found for |- ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) ) with typecode |-
7		f1f	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 ) ) : 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 ) ) with typecode |-
8	6 7	syl	Could not format ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) ) : No typesetting found for |- ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) ) with typecode |-
9		fveq2	Could not format ( g = ( oppFunc ` f ) -> ( ( oppFunc |` ( C Func D ) ) ` g ) = ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) ) : No typesetting found for |- ( g = ( oppFunc ` f ) -> ( ( oppFunc |` ( C Func D ) ) ` g ) = ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) ) with typecode |-
10	9	eqeq2d	Could not format ( g = ( oppFunc ` f ) -> ( f = ( ( oppFunc |` ( C Func D ) ) ` g ) <-> f = ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) ) ) : No typesetting found for |- ( g = ( oppFunc ` f ) -> ( f = ( ( oppFunc |` ( C Func D ) ) ` g ) <-> f = ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) ) ) with typecode |-
11	3	adantr	$$⊢\left(\phi \wedge f\in \left(O\mathrm{Func}P\right)\right)\to C\in V$$
12	4	adantr	$$⊢\left(\phi \wedge f\in \left(O\mathrm{Func}P\right)\right)\to D\in W$$
13		simpr	$$⊢\left(\phi \wedge f\in \left(O\mathrm{Func}P\right)\right)\to f\in \left(O\mathrm{Func}P\right)$$
14	1 2 11 12 13	2oppffunc	Could not format ( ( ph /\ f e. ( O Func P ) ) -> ( oppFunc ` f ) e. ( C Func D ) ) : No typesetting found for |- ( ( ph /\ f e. ( O Func P ) ) -> ( oppFunc ` f ) e. ( C Func D ) ) with typecode |-
15	14	fvresd	Could not format ( ( ph /\ f e. ( O Func P ) ) -> ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) = ( oppFunc ` ( oppFunc ` f ) ) ) : No typesetting found for |- ( ( ph /\ f e. ( O Func P ) ) -> ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) = ( oppFunc ` ( oppFunc ` f ) ) ) with typecode |-
16		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
17		eqid	Could not format ( oppFunc ` f ) = ( oppFunc ` f ) : No typesetting found for |- ( oppFunc ` f ) = ( oppFunc ` f ) with typecode |-
18	14 16 17	2oppf	Could not format ( ( ph /\ f e. ( O Func P ) ) -> ( oppFunc ` ( oppFunc ` f ) ) = f ) : No typesetting found for |- ( ( ph /\ f e. ( O Func P ) ) -> ( oppFunc ` ( oppFunc ` f ) ) = f ) with typecode |-
19	15 18	eqtr2d	Could not format ( ( ph /\ f e. ( O Func P ) ) -> f = ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) ) : No typesetting found for |- ( ( ph /\ f e. ( O Func P ) ) -> f = ( ( oppFunc |` ( C Func D ) ) ` ( oppFunc ` f ) ) ) with typecode |-
20	10 14 19	rspcedvdw	Could not format ( ( ph /\ f e. ( O Func P ) ) -> E. g e. ( C Func D ) f = ( ( oppFunc |` ( C Func D ) ) ` g ) ) : No typesetting found for |- ( ( ph /\ f e. ( O Func P ) ) -> E. g e. ( C Func D ) f = ( ( oppFunc |` ( C Func D ) ) ` g ) ) with typecode |-
21	20	ralrimiva	Could not format ( ph -> A. f e. ( O Func P ) E. g e. ( C Func D ) f = ( ( oppFunc |` ( C Func D ) ) ` g ) ) : No typesetting found for |- ( ph -> A. f e. ( O Func P ) E. g e. ( C Func D ) f = ( ( oppFunc |` ( C Func D ) ) ` g ) ) with typecode |-
22		dffo3	Could not format ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -onto-> ( O Func P ) <-> ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) /\ A. f e. ( O Func P ) E. g e. ( C Func D ) f = ( ( oppFunc |` ( C Func D ) ) ` g ) ) ) : No typesetting found for |- ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -onto-> ( O Func P ) <-> ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) /\ A. f e. ( O Func P ) E. g e. ( C Func D ) f = ( ( oppFunc |` ( C Func D ) ) ` g ) ) ) with typecode |-
23	8 21 22	sylanbrc	Could not format ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -onto-> ( O Func P ) ) : No typesetting found for |- ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -onto-> ( O Func P ) ) with typecode |-
24		df-f1o	Could not format ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) <-> ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) /\ ( oppFunc |` ( C Func D ) ) : ( C Func D ) -onto-> ( O Func P ) ) ) : No typesetting found for |- ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) <-> ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) /\ ( oppFunc |` ( C Func D ) ) : ( C Func D ) -onto-> ( O Func P ) ) ) with typecode |-
25	6 23 24	sylanbrc	Could not format ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) ) : No typesetting found for |- ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) ) with typecode |-