Metamath Proof Explorer

Theorem catprs

Description: A preorder can be extracted from a category. See catprs2 for more details. (Contributed by Zhi Wang, 18-Sep-2024)

Ref Expression
Hypotheses catprs.1 
|- ( ph -> A. x e. B A. y e. B ( x .<_ y <-> ( x H y ) =/= (/) ) )
catprs.b 
|- ( ph -> B = ( Base ` C ) )
catprs.h 
|- ( ph -> H = ( Hom ` C ) )
catprs.c 
|- ( ph -> C e. Cat )
Assertion catprs 
|- ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) )

Proof

Step Hyp Ref Expression
1 catprs.1 
 |-  ( ph -> A. x e. B A. y e. B ( x .<_ y <-> ( x H y ) =/= (/) ) )
2 catprs.b 
 |-  ( ph -> B = ( Base ` C ) )
3 catprs.h 
 |-  ( ph -> H = ( Hom ` C ) )
4 catprs.c 
 |-  ( ph -> C e. Cat )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
7 eqid 
 |-  ( Id ` C ) = ( Id ` C )
8 4 adantr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> C e. Cat )
9 simpr1 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
10 2 adantr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> B = ( Base ` C ) )
11 9 10 eleqtrd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. ( Base ` C ) )
12 5 6 7 8 11 catidcl 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Id ` C ) ` X ) e. ( X ( Hom ` C ) X ) )
13 3 adantr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> H = ( Hom ` C ) )
14 13 oveqd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X H X ) = ( X ( Hom ` C ) X ) )
15 12 14 eleqtrrd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Id ` C ) ` X ) e. ( X H X ) )
16 15 ne0d 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X H X ) =/= (/) )
17 1 adantr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> A. x e. B A. y e. B ( x .<_ y <-> ( x H y ) =/= (/) ) )
18 17 9 9 catprslem 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X <-> ( X H X ) =/= (/) ) )
19 16 18 mpbird 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X .<_ X )
20 3 ad2antrr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> H = ( Hom ` C ) )
21 20 oveqd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( X H Z ) = ( X ( Hom ` C ) Z ) )
22 2 eleq2d 
 |-  ( ph -> ( X e. B <-> X e. ( Base ` C ) ) )
23 2 eleq2d 
 |-  ( ph -> ( Y e. B <-> Y e. ( Base ` C ) ) )
24 2 eleq2d 
 |-  ( ph -> ( Z e. B <-> Z e. ( Base ` C ) ) )
25 22 23 24 3anbi123d 
 |-  ( ph -> ( ( X e. B /\ Y e. B /\ Z e. B ) <-> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) ) )
26 25 pm5.32i 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) <-> ( ph /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) ) )
27 eqid 
 |-  ( comp ` C ) = ( comp ` C )
28 4 ad2antrr 
 |-  ( ( ( ph /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> C e. Cat )
29 simplr1 
 |-  ( ( ( ph /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> X e. ( Base ` C ) )
30 simplr2 
 |-  ( ( ( ph /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> Y e. ( Base ` C ) )
31 simplr3 
 |-  ( ( ( ph /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> Z e. ( Base ` C ) )
32 20 oveqd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( X H Y ) = ( X ( Hom ` C ) Y ) )
33 simpr2 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
34 17 9 33 catprslem 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) )
35 34 biimpa 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .<_ Y ) -> ( X H Y ) =/= (/) )
36 35 adantrr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( X H Y ) =/= (/) )
37 32 36 eqnetrrd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( X ( Hom ` C ) Y ) =/= (/) )
38 26 37 sylanbr 
 |-  ( ( ( ph /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( X ( Hom ` C ) Y ) =/= (/) )
39 20 oveqd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( Y H Z ) = ( Y ( Hom ` C ) Z ) )
40 simpr3 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
41 17 33 40 catprslem 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .<_ Z <-> ( Y H Z ) =/= (/) ) )
42 41 biimpa 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ Y .<_ Z ) -> ( Y H Z ) =/= (/) )
43 42 adantrl 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( Y H Z ) =/= (/) )
44 39 43 eqnetrrd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( Y ( Hom ` C ) Z ) =/= (/) )
45 26 44 sylanbr 
 |-  ( ( ( ph /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( Y ( Hom ` C ) Z ) =/= (/) )
46 5 6 27 28 29 30 31 38 45 catcone0 
 |-  ( ( ( ph /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( X ( Hom ` C ) Z ) =/= (/) )
47 26 46 sylanb 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( X ( Hom ` C ) Z ) =/= (/) )
48 21 47 eqnetrd 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( X H Z ) =/= (/) )
49 17 9 40 catprslem 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Z <-> ( X H Z ) =/= (/) ) )
50 49 adantr 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> ( X .<_ Z <-> ( X H Z ) =/= (/) ) )
51 48 50 mpbird 
 |-  ( ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> X .<_ Z )
52 51 ex 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) )
53 19 52 jca 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) )