Theorem oppc1stflem

Description: A utility theorem for proving theorems on projection functors of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	oppc1stf.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppc1stf.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	oppc1stf.c	$$⊢\phi \to C\in V$$
	oppc1stf.d	$$⊢\phi \to D\in W$$
	oppc1stflem.1	No typesetting found for |- ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) with typecode |-
	oppc1stflem.f	$$⊢F=\left(c\in \mathrm{Cat},d\in \mathrm{Cat}⟼Y\right)$$
Assertion	oppc1stflem	Could not format assertion : No typesetting found for |- ( ph -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oppc1stf.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppc1stf.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		oppc1stf.c	$$⊢\phi \to C\in V$$
4		oppc1stf.d	$$⊢\phi \to D\in W$$
5		oppc1stflem.1	Could not format ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) : No typesetting found for |- ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) with typecode |-
6		oppc1stflem.f	$$⊢F=\left(c\in \mathrm{Cat},d\in \mathrm{Cat}⟼Y\right)$$
7		eqid	Could not format ( oppFunc ` ( C F D ) ) = ( oppFunc ` ( C F D ) ) : No typesetting found for |- ( oppFunc ` ( C F D ) ) = ( oppFunc ` ( C F D ) ) with typecode |-
8		simpr	Could not format ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> x e. ( oppFunc ` ( C F D ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> x e. ( oppFunc ` ( C F D ) ) ) with typecode |-
9	7 8	eloppf	Could not format ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> ( ( C F D ) =/= (/) /\ ( Rel ( 2nd ` ( C F D ) ) /\ Rel dom ( 2nd ` ( C F D ) ) ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> ( ( C F D ) =/= (/) /\ ( Rel ( 2nd ` ( C F D ) ) /\ Rel dom ( 2nd ` ( C F D ) ) ) ) ) with typecode |-
10	9	simpld	Could not format ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> ( C F D ) =/= (/) ) : No typesetting found for |- ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> ( C F D ) =/= (/) ) with typecode |-
11	6	mpondm0	$$⊢\neg \left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)\to CFD=\varnothing$$
12	11	necon1ai	$$⊢CFD\ne \varnothing \to \left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)$$
13	10 12	syl	Could not format ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> ( C e. Cat /\ D e. Cat ) ) : No typesetting found for |- ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> ( C e. Cat /\ D e. Cat ) ) with typecode |-
14		simplr	Could not format ( ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( oppFunc ` ( C F D ) ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( oppFunc ` ( C F D ) ) ) with typecode |-
15	5	adantlr	Could not format ( ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) with typecode |-
16	14 15	eleqtrd	Could not format ( ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( O F P ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( O F P ) ) with typecode |-
17	13 16	mpdan	Could not format ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> x e. ( O F P ) ) : No typesetting found for |- ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> x e. ( O F P ) ) with typecode |-
18	1 3	oppccatb	$$⊢\phi \to \left(C\in \mathrm{Cat}\leftrightarrow O\in \mathrm{Cat}\right)$$
19	2 4	oppccatb	$$⊢\phi \to \left(D\in \mathrm{Cat}\leftrightarrow P\in \mathrm{Cat}\right)$$
20	18 19	anbi12d	$$⊢\phi \to \left(\left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)\leftrightarrow \left(O\in \mathrm{Cat}\wedge P\in \mathrm{Cat}\right)\right)$$
21	20	biimprd	$$⊢\phi \to \left(\left(O\in \mathrm{Cat}\wedge P\in \mathrm{Cat}\right)\to \left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)\right)$$
22	6	elmpocl	$$⊢x\in \left(OFP\right)\to \left(O\in \mathrm{Cat}\wedge P\in \mathrm{Cat}\right)$$
23	21 22	impel	$$⊢\left(\phi \wedge x\in \left(OFP\right)\right)\to \left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)$$
24		simplr	$$⊢\left(\left(\phi \wedge x\in \left(OFP\right)\right)\wedge \left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)\right)\to x\in \left(OFP\right)$$
25	5	adantlr	Could not format ( ( ( ph /\ x e. ( O F P ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( O F P ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) with typecode |-
26	24 25	eleqtrrd	Could not format ( ( ( ph /\ x e. ( O F P ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( oppFunc ` ( C F D ) ) ) : No typesetting found for |- ( ( ( ph /\ x e. ( O F P ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( oppFunc ` ( C F D ) ) ) with typecode |-
27	23 26	mpdan	Could not format ( ( ph /\ x e. ( O F P ) ) -> x e. ( oppFunc ` ( C F D ) ) ) : No typesetting found for |- ( ( ph /\ x e. ( O F P ) ) -> x e. ( oppFunc ` ( C F D ) ) ) with typecode |-
28	17 27	impbida	Could not format ( ph -> ( x e. ( oppFunc ` ( C F D ) ) <-> x e. ( O F P ) ) ) : No typesetting found for |- ( ph -> ( x e. ( oppFunc ` ( C F D ) ) <-> x e. ( O F P ) ) ) with typecode |-
29	28	eqrdv	Could not format ( ph -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) : No typesetting found for |- ( ph -> ( oppFunc ` ( C F D ) ) = ( O F P ) ) with typecode |-