Metamath Proof Explorer

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 = ( oppCat ` C )
oppc1stf.p 
|- P = ( oppCat ` D )
oppc1stf.c 
|- ( ph -> C e. V )
oppc1stf.d 
|- ( ph -> D e. W )
oppc1stflem.1 
|- ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) )
oppc1stflem.f 
|- F = ( c e. Cat , d e. Cat |-> Y )
Assertion oppc1stflem 
|- ( ph -> ( oppFunc ` ( C F D ) ) = ( O F P ) )

Proof

Step Hyp Ref Expression
1 oppc1stf.o 
 |-  O = ( oppCat ` C )
2 oppc1stf.p 
 |-  P = ( oppCat ` D )
3 oppc1stf.c 
 |-  ( ph -> C e. V )
4 oppc1stf.d 
 |-  ( ph -> D e. W )
5 oppc1stflem.1 
 |-  ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) )
6 oppc1stflem.f 
 |-  F = ( c e. Cat , d e. Cat |-> Y )
7 eqid 
 |-  ( oppFunc ` ( C F D ) ) = ( oppFunc ` ( C F D ) )
8 simpr 
 |-  ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> x e. ( oppFunc ` ( C F D ) ) )
9 7 8 eloppf 
 |-  ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> ( ( C F D ) =/= (/) /\ ( Rel ( 2nd ` ( C F D ) ) /\ Rel dom ( 2nd ` ( C F D ) ) ) ) )
10 9 simpld 
 |-  ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> ( C F D ) =/= (/) )
11 6 mpondm0 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C F D ) = (/) )
12 11 necon1ai 
 |-  ( ( C F D ) =/= (/) -> ( C e. Cat /\ D e. Cat ) )
13 10 12 syl 
 |-  ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> ( C e. Cat /\ D e. Cat ) )
14 simplr 
 |-  ( ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( oppFunc ` ( C F D ) ) )
15 5 adantlr 
 |-  ( ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) )
16 14 15 eleqtrd 
 |-  ( ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( O F P ) )
17 13 16 mpdan 
 |-  ( ( ph /\ x e. ( oppFunc ` ( C F D ) ) ) -> x e. ( O F P ) )
18 1 3 oppccatb 
 |-  ( ph -> ( C e. Cat <-> O e. Cat ) )
19 2 4 oppccatb 
 |-  ( ph -> ( D e. Cat <-> P e. Cat ) )
20 18 19 anbi12d 
 |-  ( ph -> ( ( C e. Cat /\ D e. Cat ) <-> ( O e. Cat /\ P e. Cat ) ) )
21 20 biimprd 
 |-  ( ph -> ( ( O e. Cat /\ P e. Cat ) -> ( C e. Cat /\ D e. Cat ) ) )
22 6 elmpocl 
 |-  ( x e. ( O F P ) -> ( O e. Cat /\ P e. Cat ) )
23 21 22 impel 
 |-  ( ( ph /\ x e. ( O F P ) ) -> ( C e. Cat /\ D e. Cat ) )
24 simplr 
 |-  ( ( ( ph /\ x e. ( O F P ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( O F P ) )
25 5 adantlr 
 |-  ( ( ( ph /\ x e. ( O F P ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C F D ) ) = ( O F P ) )
26 24 25 eleqtrrd 
 |-  ( ( ( ph /\ x e. ( O F P ) ) /\ ( C e. Cat /\ D e. Cat ) ) -> x e. ( oppFunc ` ( C F D ) ) )
27 23 26 mpdan 
 |-  ( ( ph /\ x e. ( O F P ) ) -> x e. ( oppFunc ` ( C F D ) ) )
28 17 27 impbida 
 |-  ( ph -> ( x e. ( oppFunc ` ( C F D ) ) <-> x e. ( O F P ) ) )
29 28 eqrdv 
 |-  ( ph -> ( oppFunc ` ( C F D ) ) = ( O F P ) )