swopo

Description: A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Hypotheses	swopo.1	$⊢ (φ \land (y \in A \land z \in A)) \to (y R z \to \neg z R y)$
	swopo.2	$⊢ (φ \land (x \in A \land y \in A \land z \in A)) \to (x R y \to (x R z \lor z R y))$
Assertion	swopo	$⊢ φ \to R Po A$

Proof

Step	Hyp	Ref	Expression
1		swopo.1	$⊢ (φ \land (y \in A \land z \in A)) \to (y R z \to \neg z R y)$
2		swopo.2	$⊢ (φ \land (x \in A \land y \in A \land z \in A)) \to (x R y \to (x R z \lor z R y))$
3		id	$⊢ x \in A \to x \in A$
4	3	ancli	$⊢ x \in A \to (x \in A \land x \in A)$
5	1	ralrimivva	$⊢ φ \to \forall y \in A \forall z \in A (y R z \to \neg z R y)$
6		breq1	$⊢ y = x \to (y R z \leftrightarrow x R z)$
7		breq2	$⊢ y = x \to (z R y \leftrightarrow z R x)$
8	7	notbid	$⊢ y = x \to (\neg z R y \leftrightarrow \neg z R x)$
9	6 8	imbi12d	$⊢ y = x \to ((y R z \to \neg z R y) \leftrightarrow (x R z \to \neg z R x))$
10		breq2	$⊢ z = x \to (x R z \leftrightarrow x R x)$
11		breq1	$⊢ z = x \to (z R x \leftrightarrow x R x)$
12	11	notbid	$⊢ z = x \to (\neg z R x \leftrightarrow \neg x R x)$
13	10 12	imbi12d	$⊢ z = x \to ((x R z \to \neg z R x) \leftrightarrow (x R x \to \neg x R x))$
14	9 13	rspc2va	$⊢ ((x \in A \land x \in A) \land \forall y \in A \forall z \in A (y R z \to \neg z R y)) \to (x R x \to \neg x R x)$
15	4 5 14	syl2anr	$⊢ (φ \land x \in A) \to (x R x \to \neg x R x)$
16	15	pm2.01d	$⊢ (φ \land x \in A) \to \neg x R x$
17	1	3adantr1	$⊢ (φ \land (x \in A \land y \in A \land z \in A)) \to (y R z \to \neg z R y)$
18	2	imp	$⊢ ((φ \land (x \in A \land y \in A \land z \in A)) \land x R y) \to (x R z \lor z R y)$
19	18	orcomd	$⊢ ((φ \land (x \in A \land y \in A \land z \in A)) \land x R y) \to (z R y \lor x R z)$
20	19	ord	$⊢ ((φ \land (x \in A \land y \in A \land z \in A)) \land x R y) \to (\neg z R y \to x R z)$
21	20	expimpd	$⊢ (φ \land (x \in A \land y \in A \land z \in A)) \to ((x R y \land \neg z R y) \to x R z)$
22	17 21	sylan2d	$⊢ (φ \land (x \in A \land y \in A \land z \in A)) \to ((x R y \land y R z) \to x R z)$
23	16 22	ispod	$⊢ φ \to R Po A$

Metamath Proof Explorer

Theorem swopo

Proof