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

Metamath Proof Explorer

Theorem swoso

Description: If the incomparability relation is equivalent to equality in a subset, then the partial order strictly orders the subset. (Contributed by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypotheses swoer.1 
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )
swoer.2 
|- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )
swoer.3 
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )
swoso.4 
|- ( ph -> Y C_ X )
swoso.5 
|- ( ( ph /\ ( x e. Y /\ y e. Y /\ x R y ) ) -> x = y )
Assertion swoso 
|- ( ph -> .< Or Y )

Proof

Step Hyp Ref Expression
1 swoer.1 
 |-  R = ( ( X X. X ) \ ( .< u. `' .< ) )
2 swoer.2 
 |-  ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )
3 swoer.3 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )
4 swoso.4 
 |-  ( ph -> Y C_ X )
5 swoso.5 
 |-  ( ( ph /\ ( x e. Y /\ y e. Y /\ x R y ) ) -> x = y )
6 2 3 swopo 
 |-  ( ph -> .< Po X )
7 poss 
 |-  ( Y C_ X -> ( .< Po X -> .< Po Y ) )
8 4 6 7 sylc 
 |-  ( ph -> .< Po Y )
9 4 sselda 
 |-  ( ( ph /\ x e. Y ) -> x e. X )
10 4 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. X )
11 9 10 anim12dan 
 |-  ( ( ph /\ ( x e. Y /\ y e. Y ) ) -> ( x e. X /\ y e. X ) )
12 1 brdifun 
 |-  ( ( x e. X /\ y e. X ) -> ( x R y <-> -. ( x .< y \/ y .< x ) ) )
13 11 12 syl 
 |-  ( ( ph /\ ( x e. Y /\ y e. Y ) ) -> ( x R y <-> -. ( x .< y \/ y .< x ) ) )
14 df-3an 
 |-  ( ( x e. Y /\ y e. Y /\ x R y ) <-> ( ( x e. Y /\ y e. Y ) /\ x R y ) )
15 14 5 sylan2br 
 |-  ( ( ph /\ ( ( x e. Y /\ y e. Y ) /\ x R y ) ) -> x = y )
16 15 expr 
 |-  ( ( ph /\ ( x e. Y /\ y e. Y ) ) -> ( x R y -> x = y ) )
17 13 16 sylbird 
 |-  ( ( ph /\ ( x e. Y /\ y e. Y ) ) -> ( -. ( x .< y \/ y .< x ) -> x = y ) )
18 17 orrd 
 |-  ( ( ph /\ ( x e. Y /\ y e. Y ) ) -> ( ( x .< y \/ y .< x ) \/ x = y ) )
19 3orcomb 
 |-  ( ( x .< y \/ x = y \/ y .< x ) <-> ( x .< y \/ y .< x \/ x = y ) )
20 df-3or 
 |-  ( ( x .< y \/ y .< x \/ x = y ) <-> ( ( x .< y \/ y .< x ) \/ x = y ) )
21 19 20 bitri 
 |-  ( ( x .< y \/ x = y \/ y .< x ) <-> ( ( x .< y \/ y .< x ) \/ x = y ) )
22 18 21 sylibr 
 |-  ( ( ph /\ ( x e. Y /\ y e. Y ) ) -> ( x .< y \/ x = y \/ y .< x ) )
23 8 22 issod 
 |-  ( ph -> .< Or Y )