pocl

Description: Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997)

		Ref	Expression
	Assertion	pocl	$⊢ R Po A \to ((B \in A \land C \in A \land D \in A) \to (\neg B R B \land ((B R C \land C R D) \to B R D)))$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ x = B \to x = B$
2	1 1	breq12d	$⊢ x = B \to (x R x \leftrightarrow B R B)$
3	2	notbid	$⊢ x = B \to (\neg x R x \leftrightarrow \neg B R B)$
4		breq1	$⊢ x = B \to (x R y \leftrightarrow B R y)$
5	4	anbi1d	$⊢ x = B \to ((x R y \land y R z) \leftrightarrow (B R y \land y R z))$
6		breq1	$⊢ x = B \to (x R z \leftrightarrow B R z)$
7	5 6	imbi12d	$⊢ x = B \to (((x R y \land y R z) \to x R z) \leftrightarrow ((B R y \land y R z) \to B R z))$
8	3 7	anbi12d	$⊢ x = B \to ((\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow (\neg B R B \land ((B R y \land y R z) \to B R z)))$
9	8	imbi2d	$⊢ x = B \to ((R Po A \to (\neg x R x \land ((x R y \land y R z) \to x R z))) \leftrightarrow (R Po A \to (\neg B R B \land ((B R y \land y R z) \to B R z))))$
10		breq2	$⊢ y = C \to (B R y \leftrightarrow B R C)$
11		breq1	$⊢ y = C \to (y R z \leftrightarrow C R z)$
12	10 11	anbi12d	$⊢ y = C \to ((B R y \land y R z) \leftrightarrow (B R C \land C R z))$
13	12	imbi1d	$⊢ y = C \to (((B R y \land y R z) \to B R z) \leftrightarrow ((B R C \land C R z) \to B R z))$
14	13	anbi2d	$⊢ y = C \to ((\neg B R B \land ((B R y \land y R z) \to B R z)) \leftrightarrow (\neg B R B \land ((B R C \land C R z) \to B R z)))$
15	14	imbi2d	$⊢ y = C \to ((R Po A \to (\neg B R B \land ((B R y \land y R z) \to B R z))) \leftrightarrow (R Po A \to (\neg B R B \land ((B R C \land C R z) \to B R z))))$
16		breq2	$⊢ z = D \to (C R z \leftrightarrow C R D)$
17	16	anbi2d	$⊢ z = D \to ((B R C \land C R z) \leftrightarrow (B R C \land C R D))$
18		breq2	$⊢ z = D \to (B R z \leftrightarrow B R D)$
19	17 18	imbi12d	$⊢ z = D \to (((B R C \land C R z) \to B R z) \leftrightarrow ((B R C \land C R D) \to B R D))$
20	19	anbi2d	$⊢ z = D \to ((\neg B R B \land ((B R C \land C R z) \to B R z)) \leftrightarrow (\neg B R B \land ((B R C \land C R D) \to B R D)))$
21	20	imbi2d	$⊢ z = D \to ((R Po A \to (\neg B R B \land ((B R C \land C R z) \to B R z))) \leftrightarrow (R Po A \to (\neg B R B \land ((B R C \land C R D) \to B R D))))$
22		df-po	$⊢ R Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
23		r3al	$⊢ \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall x \forall y \forall z ((x \in A \land y \in A \land z \in A) \to (\neg x R x \land ((x R y \land y R z) \to x R z)))$
24	22 23	sylbb	$⊢ R Po A \to \forall x \forall y \forall z ((x \in A \land y \in A \land z \in A) \to (\neg x R x \land ((x R y \land y R z) \to x R z)))$
25	24	19.21bbi	$⊢ R Po A \to \forall z ((x \in A \land y \in A \land z \in A) \to (\neg x R x \land ((x R y \land y R z) \to x R z)))$
26	25	19.21bi	$⊢ R Po A \to ((x \in A \land y \in A \land z \in A) \to (\neg x R x \land ((x R y \land y R z) \to x R z)))$
27	26	com12	$⊢ (x \in A \land y \in A \land z \in A) \to (R Po A \to (\neg x R x \land ((x R y \land y R z) \to x R z)))$
28	9 15 21 27	vtocl3ga	$⊢ (B \in A \land C \in A \land D \in A) \to (R Po A \to (\neg B R B \land ((B R C \land C R D) \to B R D)))$
29	28	com12	$⊢ R Po A \to ((B \in A \land C \in A \land D \in A) \to (\neg B R B \land ((B R C \land C R D) \to B R D)))$

Metamath Proof Explorer

Theorem pocl

Proof