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

Metamath Proof Explorer

Theorem swoord1

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 swoord1 
|- ( ph -> ( A .< C <-> B .< C ) )

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 /\ ( A e. X /\ C e. X /\ B e. X ) ) -> ( A .< C -> ( A .< B \/ B .< C ) ) )
16 7 14 5 4 15 syl13anc 
 |-  ( ph -> ( A .< C -> ( A .< B \/ B .< C ) ) )
17 1 brdifun 
 |-  ( ( A e. X /\ B e. X ) -> ( A R B <-> -. ( A .< B \/ B .< A ) ) )
18 14 4 17 syl2anc 
 |-  ( ph -> ( A R B <-> -. ( A .< B \/ B .< A ) ) )
19 6 18 mpbid 
 |-  ( ph -> -. ( A .< B \/ B .< A ) )
20 orc 
 |-  ( A .< B -> ( A .< B \/ B .< A ) )
21 19 20 nsyl 
 |-  ( ph -> -. A .< B )
22 biorf 
 |-  ( -. A .< B -> ( B .< C <-> ( A .< B \/ B .< C ) ) )
23 21 22 syl 
 |-  ( ph -> ( B .< C <-> ( A .< B \/ B .< C ) ) )
24 16 23 sylibrd 
 |-  ( ph -> ( A .< C -> B .< C ) )
25 3 swopolem 
 |-  ( ( ph /\ ( B e. X /\ C e. X /\ A e. X ) ) -> ( B .< C -> ( B .< A \/ A .< C ) ) )
26 7 4 5 14 25 syl13anc 
 |-  ( ph -> ( B .< C -> ( B .< A \/ A .< C ) ) )
27 olc 
 |-  ( B .< A -> ( A .< B \/ B .< A ) )
28 19 27 nsyl 
 |-  ( ph -> -. B .< A )
29 biorf 
 |-  ( -. B .< A -> ( A .< C <-> ( B .< A \/ A .< C ) ) )
30 28 29 syl 
 |-  ( ph -> ( A .< C <-> ( B .< A \/ A .< C ) ) )
31 26 30 sylibrd 
 |-  ( ph -> ( B .< C -> A .< C ) )
32 24 31 impbid 
 |-  ( ph -> ( A .< C <-> B .< C ) )