Metamath Proof Explorer

Theorem oppcendc

Description: The opposite category of a category whose morphisms are all endomorphisms has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses oppcendc.o 
|- O = ( oppCat ` C )
oppcendc.b 
|- B = ( Base ` C )
oppcendc.h 
|- H = ( Hom ` C )
oppcendc.1 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x =/= y -> ( x H y ) = (/) ) )
Assertion oppcendc 
|- ( ph -> ( Homf ` C ) = ( Homf ` O ) )

Proof

Step Hyp Ref Expression
1 oppcendc.o 
 |-  O = ( oppCat ` C )
2 oppcendc.b 
 |-  B = ( Base ` C )
3 oppcendc.h 
 |-  H = ( Hom ` C )
4 oppcendc.1 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x =/= y -> ( x H y ) = (/) ) )
5 4 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( x =/= y -> ( x H y ) = (/) ) )
6 eqeq12 
 |-  ( ( x = p /\ y = q ) -> ( x = y <-> p = q ) )
7 6 necon3bid 
 |-  ( ( x = p /\ y = q ) -> ( x =/= y <-> p =/= q ) )
8 oveq12 
 |-  ( ( x = p /\ y = q ) -> ( x H y ) = ( p H q ) )
9 8 eqeq1d 
 |-  ( ( x = p /\ y = q ) -> ( ( x H y ) = (/) <-> ( p H q ) = (/) ) )
10 7 9 imbi12d 
 |-  ( ( x = p /\ y = q ) -> ( ( x =/= y -> ( x H y ) = (/) ) <-> ( p =/= q -> ( p H q ) = (/) ) ) )
11 10 rspc2gv 
 |-  ( ( p e. B /\ q e. B ) -> ( A. x e. B A. y e. B ( x =/= y -> ( x H y ) = (/) ) -> ( p =/= q -> ( p H q ) = (/) ) ) )
12 5 11 mpan9 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> ( p =/= q -> ( p H q ) = (/) ) )
13 simprr 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> q e. B )
14 simprl 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> p e. B )
15 5 adantr 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> A. x e. B A. y e. B ( x =/= y -> ( x H y ) = (/) ) )
16 eqeq12 
 |-  ( ( x = q /\ y = p ) -> ( x = y <-> q = p ) )
17 equcom 
 |-  ( p = q <-> q = p )
18 16 17 bitr4di 
 |-  ( ( x = q /\ y = p ) -> ( x = y <-> p = q ) )
19 18 necon3bid 
 |-  ( ( x = q /\ y = p ) -> ( x =/= y <-> p =/= q ) )
20 oveq12 
 |-  ( ( x = q /\ y = p ) -> ( x H y ) = ( q H p ) )
21 20 eqeq1d 
 |-  ( ( x = q /\ y = p ) -> ( ( x H y ) = (/) <-> ( q H p ) = (/) ) )
22 19 21 imbi12d 
 |-  ( ( x = q /\ y = p ) -> ( ( x =/= y -> ( x H y ) = (/) ) <-> ( p =/= q -> ( q H p ) = (/) ) ) )
23 22 rspc2gv 
 |-  ( ( q e. B /\ p e. B ) -> ( A. x e. B A. y e. B ( x =/= y -> ( x H y ) = (/) ) -> ( p =/= q -> ( q H p ) = (/) ) ) )
24 23 imp 
 |-  ( ( ( q e. B /\ p e. B ) /\ A. x e. B A. y e. B ( x =/= y -> ( x H y ) = (/) ) ) -> ( p =/= q -> ( q H p ) = (/) ) )
25 13 14 15 24 syl21anc 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> ( p =/= q -> ( q H p ) = (/) ) )
26 12 25 jcad 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> ( p =/= q -> ( ( p H q ) = (/) /\ ( q H p ) = (/) ) ) )
27 nne 
 |-  ( -. p =/= q <-> p = q )
28 id 
 |-  ( p = q -> p = q )
29 equcomi 
 |-  ( p = q -> q = p )
30 28 29 oveq12d 
 |-  ( p = q -> ( p H q ) = ( q H p ) )
31 27 30 sylbi 
 |-  ( -. p =/= q -> ( p H q ) = ( q H p ) )
32 eqtr3 
 |-  ( ( ( p H q ) = (/) /\ ( q H p ) = (/) ) -> ( p H q ) = ( q H p ) )
33 31 32 ja 
 |-  ( ( p =/= q -> ( ( p H q ) = (/) /\ ( q H p ) = (/) ) ) -> ( p H q ) = ( q H p ) )
34 26 33 syl 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> ( p H q ) = ( q H p ) )
35 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
36 35 2 3 14 13 homfval 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> ( p ( Homf ` C ) q ) = ( p H q ) )
37 35 2 3 13 14 homfval 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> ( q ( Homf ` C ) p ) = ( q H p ) )
38 34 36 37 3eqtr4d 
 |-  ( ( ph /\ ( p e. B /\ q e. B ) ) -> ( p ( Homf ` C ) q ) = ( q ( Homf ` C ) p ) )
39 38 ralrimivva 
 |-  ( ph -> A. p e. B A. q e. B ( p ( Homf ` C ) q ) = ( q ( Homf ` C ) p ) )
40 35 2 homffn 
 |-  ( Homf ` C ) Fn ( B X. B )
41 tpossym 
 |-  ( ( Homf ` C ) Fn ( B X. B ) -> ( tpos ( Homf ` C ) = ( Homf ` C ) <-> A. p e. B A. q e. B ( p ( Homf ` C ) q ) = ( q ( Homf ` C ) p ) ) )
42 40 41 ax-mp 
 |-  ( tpos ( Homf ` C ) = ( Homf ` C ) <-> A. p e. B A. q e. B ( p ( Homf ` C ) q ) = ( q ( Homf ` C ) p ) )
43 39 42 sylibr 
 |-  ( ph -> tpos ( Homf ` C ) = ( Homf ` C ) )
44 1 35 oppchomf 
 |-  tpos ( Homf ` C ) = ( Homf ` O )
45 43 44 eqtr3di 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` O ) )