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 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) )
catprs.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
catprs.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
catprs.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion catprs ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 catprs.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) )
2 catprs.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
3 catprs.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
4 catprs.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
8 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐶 ∈ Cat )
9 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
10 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐶 ) )
11 9 10 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
12 5 6 7 8 11 catidcl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐻 = ( Hom ‘ 𝐶 ) )
14 13 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐻 𝑋 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
15 12 14 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
16 15 ne0d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐻 𝑋 ) ≠ ∅ )
17 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) )
18 17 9 9 catprslem ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ↔ ( 𝑋 𝐻 𝑋 ) ≠ ∅ ) )
19 16 18 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ≤ 𝑋 )
20 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → 𝐻 = ( Hom ‘ 𝐶 ) )
21 20 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑋 𝐻 𝑍 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) )
22 2 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ 𝐶 ) ) )
23 2 eleq2d ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐵 ↔ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
24 2 eleq2d ⊢ ( 𝜑 → ( 𝑍 ∈ 𝐵 ↔ 𝑍 ∈ ( Base ‘ 𝐶 ) ) )
25 22 23 24 3anbi123d ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ↔ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) ) )
26 25 pm5.32i ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) ) )
27 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
28 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → 𝐶 ∈ Cat )
29 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
30 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → 𝑌 ∈ ( Base ‘ 𝐶 ) )
31 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
32 20 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
33 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
34 17 9 33 catprslem ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) )
35 34 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 𝐻 𝑌 ) ≠ ∅ )
36 35 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑋 𝐻 𝑌 ) ≠ ∅ )
37 32 36 eqnetrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ≠ ∅ )
38 26 37 sylanbr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ≠ ∅ )
39 20 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑌 𝐻 𝑍 ) = ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
40 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
41 17 33 40 catprslem ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ≤ 𝑍 ↔ ( 𝑌 𝐻 𝑍 ) ≠ ∅ ) )
42 41 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑌 ≤ 𝑍 ) → ( 𝑌 𝐻 𝑍 ) ≠ ∅ )
43 42 adantrl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑌 𝐻 𝑍 ) ≠ ∅ )
44 39 43 eqnetrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) ≠ ∅ )
45 26 44 sylanbr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) ≠ ∅ )
46 5 6 27 28 29 30 31 38 45 catcone0 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) ≠ ∅ )
47 26 46 sylanb ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) ≠ ∅ )
48 21 47 eqnetrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑋 𝐻 𝑍 ) ≠ ∅ )
49 17 9 40 catprslem ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑍 ↔ ( 𝑋 𝐻 𝑍 ) ≠ ∅ ) )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → ( 𝑋 ≤ 𝑍 ↔ ( 𝑋 𝐻 𝑍 ) ≠ ∅ ) )
51 48 50 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) ) → 𝑋 ≤ 𝑍 )
52 51 ex ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) )
53 19 52 jca ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) ) )