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	$⊢ φ \to \forall x \in B \forall y \in B (x \underset{˙}{\leq} y \leftrightarrow x H y \neq \emptyset)$
	catprs.b	$⊢ φ \to B = {Base}_{C}$
	catprs.h	$⊢ φ \to H = Hom (C)$
	catprs.c	$⊢ φ \to C \in Cat$
Assertion	catprs	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} X \land ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} Z) \to X \underset{˙}{\leq} Z))$

Proof

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

Metamath Proof Explorer

Theorem catprs

Proof