This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )