pslem

Description: Lemma for psref and others. (Contributed by NM, 12-May-2008) (Revised by Mario Carneiro, 30-Apr-2015)

		Ref	Expression
	Assertion	pslem	$⊢ R \in PosetRel \to (((A R B \land B R C) \to A R C) \land (A \in ⋃ ⋃ R \to A R A) \land ((A R B \land B R A) \to A = B))$

Proof

Step	Hyp	Ref	Expression
1		psrel	$⊢ R \in PosetRel \to Rel R$
2		brrelex12	$⊢ (Rel R \land A R B) \to (A \in V \land B \in V)$
3	1 2	sylan	$⊢ (R \in PosetRel \land A R B) \to (A \in V \land B \in V)$
4		brrelex2	$⊢ (Rel R \land B R C) \to C \in V$
5	1 4	sylan	$⊢ (R \in PosetRel \land B R C) \to C \in V$
6	3 5	anim12dan	$⊢ (R \in PosetRel \land (A R B \land B R C)) \to ((A \in V \land B \in V) \land C \in V)$
7		pstr2	$⊢ R \in PosetRel \to R \circ R \subseteq R$
8		cotr	$⊢ R \circ R \subseteq R \leftrightarrow \forall x \forall y \forall z ((x R y \land y R z) \to x R z)$
9	7 8	sylib	$⊢ R \in PosetRel \to \forall x \forall y \forall z ((x R y \land y R z) \to x R z)$
10	9	adantr	$⊢ (R \in PosetRel \land (A R B \land B R C)) \to \forall x \forall y \forall z ((x R y \land y R z) \to x R z)$
11		simpr	$⊢ (R \in PosetRel \land (A R B \land B R C)) \to (A R B \land B R C)$
12		breq12	$⊢ (x = A \land y = B) \to (x R y \leftrightarrow A R B)$
13	12	3adant3	$⊢ (x = A \land y = B \land z = C) \to (x R y \leftrightarrow A R B)$
14		breq12	$⊢ (y = B \land z = C) \to (y R z \leftrightarrow B R C)$
15	14	3adant1	$⊢ (x = A \land y = B \land z = C) \to (y R z \leftrightarrow B R C)$
16	13 15	anbi12d	$⊢ (x = A \land y = B \land z = C) \to ((x R y \land y R z) \leftrightarrow (A R B \land B R C))$
17		breq12	$⊢ (x = A \land z = C) \to (x R z \leftrightarrow A R C)$
18	17	3adant2	$⊢ (x = A \land y = B \land z = C) \to (x R z \leftrightarrow A R C)$
19	16 18	imbi12d	$⊢ (x = A \land y = B \land z = C) \to (((x R y \land y R z) \to x R z) \leftrightarrow ((A R B \land B R C) \to A R C))$
20	19	spc3gv	$⊢ (A \in V \land B \in V \land C \in V) \to (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \to ((A R B \land B R C) \to A R C))$
21	20	3expa	$⊢ ((A \in V \land B \in V) \land C \in V) \to (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \to ((A R B \land B R C) \to A R C))$
22	6 10 11 21	syl3c	$⊢ (R \in PosetRel \land (A R B \land B R C)) \to A R C$
23	22	ex	$⊢ R \in PosetRel \to ((A R B \land B R C) \to A R C)$
24		psref2	$⊢ R \in PosetRel \to R \cap R^{-1} = {I ↾}_{⋃ ⋃ R}$
25		asymref2	$⊢ R \cap R^{-1} = {I ↾}_{⋃ ⋃ R} \leftrightarrow (\forall x \in ⋃ ⋃ R x R x \land \forall x \forall y ((x R y \land y R x) \to x = y))$
26	25	simplbi	$⊢ R \cap R^{-1} = {I ↾}_{⋃ ⋃ R} \to \forall x \in ⋃ ⋃ R x R x$
27		breq12	$⊢ (x = A \land x = A) \to (x R x \leftrightarrow A R A)$
28	27	anidms	$⊢ x = A \to (x R x \leftrightarrow A R A)$
29	28	rspccv	$⊢ \forall x \in ⋃ ⋃ R x R x \to (A \in ⋃ ⋃ R \to A R A)$
30	24 26 29	3syl	$⊢ R \in PosetRel \to (A \in ⋃ ⋃ R \to A R A)$
31	3	adantrr	$⊢ (R \in PosetRel \land (A R B \land B R A)) \to (A \in V \land B \in V)$
32	25	simprbi	$⊢ R \cap R^{-1} = {I ↾}_{⋃ ⋃ R} \to \forall x \forall y ((x R y \land y R x) \to x = y)$
33	24 32	syl	$⊢ R \in PosetRel \to \forall x \forall y ((x R y \land y R x) \to x = y)$
34	33	adantr	$⊢ (R \in PosetRel \land (A R B \land B R A)) \to \forall x \forall y ((x R y \land y R x) \to x = y)$
35		simpr	$⊢ (R \in PosetRel \land (A R B \land B R A)) \to (A R B \land B R A)$
36		breq12	$⊢ (y = B \land x = A) \to (y R x \leftrightarrow B R A)$
37	36	ancoms	$⊢ (x = A \land y = B) \to (y R x \leftrightarrow B R A)$
38	12 37	anbi12d	$⊢ (x = A \land y = B) \to ((x R y \land y R x) \leftrightarrow (A R B \land B R A))$
39		eqeq12	$⊢ (x = A \land y = B) \to (x = y \leftrightarrow A = B)$
40	38 39	imbi12d	$⊢ (x = A \land y = B) \to (((x R y \land y R x) \to x = y) \leftrightarrow ((A R B \land B R A) \to A = B))$
41	40	spc2gv	$⊢ (A \in V \land B \in V) \to (\forall x \forall y ((x R y \land y R x) \to x = y) \to ((A R B \land B R A) \to A = B))$
42	31 34 35 41	syl3c	$⊢ (R \in PosetRel \land (A R B \land B R A)) \to A = B$
43	42	ex	$⊢ R \in PosetRel \to ((A R B \land B R A) \to A = B)$
44	23 30 43	3jca	$⊢ R \in PosetRel \to (((A R B \land B R C) \to A R C) \land (A \in ⋃ ⋃ R \to A R A) \land ((A R B \land B R A) \to A = B))$

Metamath Proof Explorer

Theorem pslem

Proof