Metamath Proof Explorer


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 )