Theorem swopo

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

	Ref	Expression
Hypotheses	swopo.1	|- ( ( ph /\ ( y e. A /\ z e. A ) ) -> ( y R z -> -. z R y ) )
	swopo.2	|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x R y -> ( x R z \/ z R y ) ) )
Assertion	swopo	|- ( ph -> R Po A )

Proof

Step	Hyp	Ref	Expression
1		swopo.1	|- ( ( ph /\ ( y e. A /\ z e. A ) ) -> ( y R z -> -. z R y ) )
2		swopo.2	|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x R y -> ( x R z \/ z R y ) ) )
3		id	|- ( x e. A -> x e. A )
4	3	ancli	|- ( x e. A -> ( x e. A /\ x e. A ) )
5	1	ralrimivva	|- ( ph -> A. y e. A A. z e. A ( y R z -> -. z R y ) )
6		breq1	|- ( y = x -> ( y R z <-> x R z ) )
7		breq2	|- ( y = x -> ( z R y <-> z R x ) )
8	7	notbid	|- ( y = x -> ( -. z R y <-> -. z R x ) )
9	6 8	imbi12d	|- ( y = x -> ( ( y R z -> -. z R y ) <-> ( x R z -> -. z R x ) ) )
10		breq2	|- ( z = x -> ( x R z <-> x R x ) )
11		breq1	|- ( z = x -> ( z R x <-> x R x ) )
12	11	notbid	|- ( z = x -> ( -. z R x <-> -. x R x ) )
13	10 12	imbi12d	|- ( z = x -> ( ( x R z -> -. z R x ) <-> ( x R x -> -. x R x ) ) )
14	9 13	rspc2va	|- ( ( ( x e. A /\ x e. A ) /\ A. y e. A A. z e. A ( y R z -> -. z R y ) ) -> ( x R x -> -. x R x ) )
15	4 5 14	syl2anr	|- ( ( ph /\ x e. A ) -> ( x R x -> -. x R x ) )
16	15	pm2.01d	|- ( ( ph /\ x e. A ) -> -. x R x )
17	1	3adantr1	|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( y R z -> -. z R y ) )
18	2	imp	|- ( ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ x R y ) -> ( x R z \/ z R y ) )
19	18	orcomd	|- ( ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ x R y ) -> ( z R y \/ x R z ) )
20	19	ord	|- ( ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ x R y ) -> ( -. z R y -> x R z ) )
21	20	expimpd	|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x R y /\ -. z R y ) -> x R z ) )
22	17 21	sylan2d	|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x R y /\ y R z ) -> x R z ) )
23	16 22	ispod	|- ( ph -> R Po A )