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

Metamath Proof Explorer

Theorem swoord2

Description: The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-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 ) ) )
swoord.4 
|- ( ph -> B e. X )
swoord.5 
|- ( ph -> C e. X )
swoord.6 
|- ( ph -> A R B )
Assertion swoord2 
|- ( ph -> ( C .< A <-> C .< B ) )

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 swoord.4 
 |-  ( ph -> B e. X )
5 swoord.5 
 |-  ( ph -> C e. X )
6 swoord.6 
 |-  ( ph -> A R B )
7 id 
 |-  ( ph -> ph )
8 difss 
 |-  ( ( X X. X ) \ ( .< u. `' .< ) ) C_ ( X X. X )
9 1 8 eqsstri 
 |-  R C_ ( X X. X )
10 9 ssbri 
 |-  ( A R B -> A ( X X. X ) B )
11 df-br 
 |-  ( A ( X X. X ) B <-> <. A , B >. e. ( X X. X ) )
12 opelxp1 
 |-  ( <. A , B >. e. ( X X. X ) -> A e. X )
13 11 12 sylbi 
 |-  ( A ( X X. X ) B -> A e. X )
14 6 10 13 3syl 
 |-  ( ph -> A e. X )
15 3 swopolem 
 |-  ( ( ph /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( C .< A -> ( C .< B \/ B .< A ) ) )
16 7 5 14 4 15 syl13anc 
 |-  ( ph -> ( C .< A -> ( C .< B \/ B .< A ) ) )
17 idd 
 |-  ( ph -> ( C .< B -> C .< B ) )
18 1 brdifun 
 |-  ( ( A e. X /\ B e. X ) -> ( A R B <-> -. ( A .< B \/ B .< A ) ) )
19 14 4 18 syl2anc 
 |-  ( ph -> ( A R B <-> -. ( A .< B \/ B .< A ) ) )
20 6 19 mpbid 
 |-  ( ph -> -. ( A .< B \/ B .< A ) )
21 olc 
 |-  ( B .< A -> ( A .< B \/ B .< A ) )
22 20 21 nsyl 
 |-  ( ph -> -. B .< A )
23 22 pm2.21d 
 |-  ( ph -> ( B .< A -> C .< B ) )
24 17 23 jaod 
 |-  ( ph -> ( ( C .< B \/ B .< A ) -> C .< B ) )
25 16 24 syld 
 |-  ( ph -> ( C .< A -> C .< B ) )
26 3 swopolem 
 |-  ( ( ph /\ ( C e. X /\ B e. X /\ A e. X ) ) -> ( C .< B -> ( C .< A \/ A .< B ) ) )
27 7 5 4 14 26 syl13anc 
 |-  ( ph -> ( C .< B -> ( C .< A \/ A .< B ) ) )
28 idd 
 |-  ( ph -> ( C .< A -> C .< A ) )
29 orc 
 |-  ( A .< B -> ( A .< B \/ B .< A ) )
30 20 29 nsyl 
 |-  ( ph -> -. A .< B )
31 30 pm2.21d 
 |-  ( ph -> ( A .< B -> C .< A ) )
32 28 31 jaod 
 |-  ( ph -> ( ( C .< A \/ A .< B ) -> C .< A ) )
33 27 32 syld 
 |-  ( ph -> ( C .< B -> C .< A ) )
34 25 33 impbid 
 |-  ( ph -> ( C .< A <-> C .< B ) )