Metamath Proof Explorer

Theorem swoer

Description: Incomparability under a strict weak partial order is an equivalence relation. (Contributed by Mario Carneiro, 9-Jul-2014) (Revised by Mario Carneiro, 12-Aug-2015)

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 ) ) )
Assertion swoer 
|- ( ph -> R Er X )

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 difss 
 |-  ( ( X X. X ) \ ( .< u. `' .< ) ) C_ ( X X. X )
5 1 4 eqsstri 
 |-  R C_ ( X X. X )
6 relxp 
 |-  Rel ( X X. X )
7 relss 
 |-  ( R C_ ( X X. X ) -> ( Rel ( X X. X ) -> Rel R ) )
8 5 6 7 mp2 
 |-  Rel R
9 8 a1i 
 |-  ( ph -> Rel R )
10 simpr 
 |-  ( ( ph /\ u R v ) -> u R v )
11 orcom 
 |-  ( ( u .< v \/ v .< u ) <-> ( v .< u \/ u .< v ) )
12 11 a1i 
 |-  ( ( ph /\ u R v ) -> ( ( u .< v \/ v .< u ) <-> ( v .< u \/ u .< v ) ) )
13 12 notbid 
 |-  ( ( ph /\ u R v ) -> ( -. ( u .< v \/ v .< u ) <-> -. ( v .< u \/ u .< v ) ) )
14 5 ssbri 
 |-  ( u R v -> u ( X X. X ) v )
15 14 adantl 
 |-  ( ( ph /\ u R v ) -> u ( X X. X ) v )
16 brxp 
 |-  ( u ( X X. X ) v <-> ( u e. X /\ v e. X ) )
17 15 16 sylib 
 |-  ( ( ph /\ u R v ) -> ( u e. X /\ v e. X ) )
18 1 brdifun 
 |-  ( ( u e. X /\ v e. X ) -> ( u R v <-> -. ( u .< v \/ v .< u ) ) )
19 17 18 syl 
 |-  ( ( ph /\ u R v ) -> ( u R v <-> -. ( u .< v \/ v .< u ) ) )
20 17 simprd 
 |-  ( ( ph /\ u R v ) -> v e. X )
21 17 simpld 
 |-  ( ( ph /\ u R v ) -> u e. X )
22 1 brdifun 
 |-  ( ( v e. X /\ u e. X ) -> ( v R u <-> -. ( v .< u \/ u .< v ) ) )
23 20 21 22 syl2anc 
 |-  ( ( ph /\ u R v ) -> ( v R u <-> -. ( v .< u \/ u .< v ) ) )
24 13 19 23 3bitr4d 
 |-  ( ( ph /\ u R v ) -> ( u R v <-> v R u ) )
25 10 24 mpbid 
 |-  ( ( ph /\ u R v ) -> v R u )
26 simprl 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> u R v )
27 14 ad2antrl 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> u ( X X. X ) v )
28 16 simplbi 
 |-  ( u ( X X. X ) v -> u e. X )
29 27 28 syl 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> u e. X )
30 16 simprbi 
 |-  ( u ( X X. X ) v -> v e. X )
31 27 30 syl 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> v e. X )
32 29 31 18 syl2anc 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> ( u R v <-> -. ( u .< v \/ v .< u ) ) )
33 26 32 mpbid 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> -. ( u .< v \/ v .< u ) )
34 simprr 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> v R w )
35 5 brel 
 |-  ( v R w -> ( v e. X /\ w e. X ) )
36 35 simprd 
 |-  ( v R w -> w e. X )
37 34 36 syl 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> w e. X )
38 1 brdifun 
 |-  ( ( v e. X /\ w e. X ) -> ( v R w <-> -. ( v .< w \/ w .< v ) ) )
39 31 37 38 syl2anc 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> ( v R w <-> -. ( v .< w \/ w .< v ) ) )
40 34 39 mpbid 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> -. ( v .< w \/ w .< v ) )
41 simpl 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> ph )
42 3 swopolem 
 |-  ( ( ph /\ ( u e. X /\ w e. X /\ v e. X ) ) -> ( u .< w -> ( u .< v \/ v .< w ) ) )
43 41 29 37 31 42 syl13anc 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> ( u .< w -> ( u .< v \/ v .< w ) ) )
44 3 swopolem 
 |-  ( ( ph /\ ( w e. X /\ u e. X /\ v e. X ) ) -> ( w .< u -> ( w .< v \/ v .< u ) ) )
45 41 37 29 31 44 syl13anc 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> ( w .< u -> ( w .< v \/ v .< u ) ) )
46 orcom 
 |-  ( ( v .< u \/ w .< v ) <-> ( w .< v \/ v .< u ) )
47 45 46 imbitrrdi 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> ( w .< u -> ( v .< u \/ w .< v ) ) )
48 43 47 orim12d 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> ( ( u .< w \/ w .< u ) -> ( ( u .< v \/ v .< w ) \/ ( v .< u \/ w .< v ) ) ) )
49 or4 
 |-  ( ( ( u .< v \/ v .< w ) \/ ( v .< u \/ w .< v ) ) <-> ( ( u .< v \/ v .< u ) \/ ( v .< w \/ w .< v ) ) )
50 48 49 imbitrdi 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> ( ( u .< w \/ w .< u ) -> ( ( u .< v \/ v .< u ) \/ ( v .< w \/ w .< v ) ) ) )
51 33 40 50 mtord 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> -. ( u .< w \/ w .< u ) )
52 1 brdifun 
 |-  ( ( u e. X /\ w e. X ) -> ( u R w <-> -. ( u .< w \/ w .< u ) ) )
53 29 37 52 syl2anc 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> ( u R w <-> -. ( u .< w \/ w .< u ) ) )
54 51 53 mpbird 
 |-  ( ( ph /\ ( u R v /\ v R w ) ) -> u R w )
55 2 3 swopo 
 |-  ( ph -> .< Po X )
56 poirr 
 |-  ( ( .< Po X /\ u e. X ) -> -. u .< u )
57 55 56 sylan 
 |-  ( ( ph /\ u e. X ) -> -. u .< u )
58 pm1.2 
 |-  ( ( u .< u \/ u .< u ) -> u .< u )
59 57 58 nsyl 
 |-  ( ( ph /\ u e. X ) -> -. ( u .< u \/ u .< u ) )
60 simpr 
 |-  ( ( ph /\ u e. X ) -> u e. X )
61 1 brdifun 
 |-  ( ( u e. X /\ u e. X ) -> ( u R u <-> -. ( u .< u \/ u .< u ) ) )
62 60 60 61 syl2anc 
 |-  ( ( ph /\ u e. X ) -> ( u R u <-> -. ( u .< u \/ u .< u ) ) )
63 59 62 mpbird 
 |-  ( ( ph /\ u e. X ) -> u R u )
64 5 ssbri 
 |-  ( u R u -> u ( X X. X ) u )
65 brxp 
 |-  ( u ( X X. X ) u <-> ( u e. X /\ u e. X ) )
66 65 simplbi 
 |-  ( u ( X X. X ) u -> u e. X )
67 64 66 syl 
 |-  ( u R u -> u e. X )
68 67 adantl 
 |-  ( ( ph /\ u R u ) -> u e. X )
69 63 68 impbida 
 |-  ( ph -> ( u e. X <-> u R u ) )
70 9 25 54 69 iserd 
 |-  ( ph -> R Er X )