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 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < < ) )
swoer.2 ( ( 𝜑 ∧ ( 𝑦𝑋𝑧𝑋 ) ) → ( 𝑦 < 𝑧 → ¬ 𝑧 < 𝑦 ) )
swoer.3 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑥 < 𝑦 → ( 𝑥 < 𝑧𝑧 < 𝑦 ) ) )
Assertion swoer ( 𝜑𝑅 Er 𝑋 )

Proof

Step Hyp Ref Expression
1 swoer.1 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < < ) )
2 swoer.2 ( ( 𝜑 ∧ ( 𝑦𝑋𝑧𝑋 ) ) → ( 𝑦 < 𝑧 → ¬ 𝑧 < 𝑦 ) )
3 swoer.3 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑥 < 𝑦 → ( 𝑥 < 𝑧𝑧 < 𝑦 ) ) )
4 difss ( ( 𝑋 × 𝑋 ) ∖ ( < < ) ) ⊆ ( 𝑋 × 𝑋 )
5 1 4 eqsstri 𝑅 ⊆ ( 𝑋 × 𝑋 )
6 relxp Rel ( 𝑋 × 𝑋 )
7 relss ( 𝑅 ⊆ ( 𝑋 × 𝑋 ) → ( Rel ( 𝑋 × 𝑋 ) → Rel 𝑅 ) )
8 5 6 7 mp2 Rel 𝑅
9 8 a1i ( 𝜑 → Rel 𝑅 )
10 simpr ( ( 𝜑𝑢 𝑅 𝑣 ) → 𝑢 𝑅 𝑣 )
11 orcom ( ( 𝑢 < 𝑣𝑣 < 𝑢 ) ↔ ( 𝑣 < 𝑢𝑢 < 𝑣 ) )
12 11 a1i ( ( 𝜑𝑢 𝑅 𝑣 ) → ( ( 𝑢 < 𝑣𝑣 < 𝑢 ) ↔ ( 𝑣 < 𝑢𝑢 < 𝑣 ) ) )
13 12 notbid ( ( 𝜑𝑢 𝑅 𝑣 ) → ( ¬ ( 𝑢 < 𝑣𝑣 < 𝑢 ) ↔ ¬ ( 𝑣 < 𝑢𝑢 < 𝑣 ) ) )
14 5 ssbri ( 𝑢 𝑅 𝑣𝑢 ( 𝑋 × 𝑋 ) 𝑣 )
15 14 adantl ( ( 𝜑𝑢 𝑅 𝑣 ) → 𝑢 ( 𝑋 × 𝑋 ) 𝑣 )
16 brxp ( 𝑢 ( 𝑋 × 𝑋 ) 𝑣 ↔ ( 𝑢𝑋𝑣𝑋 ) )
17 15 16 sylib ( ( 𝜑𝑢 𝑅 𝑣 ) → ( 𝑢𝑋𝑣𝑋 ) )
18 1 brdifun ( ( 𝑢𝑋𝑣𝑋 ) → ( 𝑢 𝑅 𝑣 ↔ ¬ ( 𝑢 < 𝑣𝑣 < 𝑢 ) ) )
19 17 18 syl ( ( 𝜑𝑢 𝑅 𝑣 ) → ( 𝑢 𝑅 𝑣 ↔ ¬ ( 𝑢 < 𝑣𝑣 < 𝑢 ) ) )
20 17 simprd ( ( 𝜑𝑢 𝑅 𝑣 ) → 𝑣𝑋 )
21 17 simpld ( ( 𝜑𝑢 𝑅 𝑣 ) → 𝑢𝑋 )
22 1 brdifun ( ( 𝑣𝑋𝑢𝑋 ) → ( 𝑣 𝑅 𝑢 ↔ ¬ ( 𝑣 < 𝑢𝑢 < 𝑣 ) ) )
23 20 21 22 syl2anc ( ( 𝜑𝑢 𝑅 𝑣 ) → ( 𝑣 𝑅 𝑢 ↔ ¬ ( 𝑣 < 𝑢𝑢 < 𝑣 ) ) )
24 13 19 23 3bitr4d ( ( 𝜑𝑢 𝑅 𝑣 ) → ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑢 ) )
25 10 24 mpbid ( ( 𝜑𝑢 𝑅 𝑣 ) → 𝑣 𝑅 𝑢 )
26 simprl ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → 𝑢 𝑅 𝑣 )
27 14 ad2antrl ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → 𝑢 ( 𝑋 × 𝑋 ) 𝑣 )
28 16 simplbi ( 𝑢 ( 𝑋 × 𝑋 ) 𝑣𝑢𝑋 )
29 27 28 syl ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → 𝑢𝑋 )
30 16 simprbi ( 𝑢 ( 𝑋 × 𝑋 ) 𝑣𝑣𝑋 )
31 27 30 syl ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → 𝑣𝑋 )
32 29 31 18 syl2anc ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ( 𝑢 𝑅 𝑣 ↔ ¬ ( 𝑢 < 𝑣𝑣 < 𝑢 ) ) )
33 26 32 mpbid ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ¬ ( 𝑢 < 𝑣𝑣 < 𝑢 ) )
34 simprr ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → 𝑣 𝑅 𝑤 )
35 5 brel ( 𝑣 𝑅 𝑤 → ( 𝑣𝑋𝑤𝑋 ) )
36 35 simprd ( 𝑣 𝑅 𝑤𝑤𝑋 )
37 34 36 syl ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → 𝑤𝑋 )
38 1 brdifun ( ( 𝑣𝑋𝑤𝑋 ) → ( 𝑣 𝑅 𝑤 ↔ ¬ ( 𝑣 < 𝑤𝑤 < 𝑣 ) ) )
39 31 37 38 syl2anc ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ( 𝑣 𝑅 𝑤 ↔ ¬ ( 𝑣 < 𝑤𝑤 < 𝑣 ) ) )
40 34 39 mpbid ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ¬ ( 𝑣 < 𝑤𝑤 < 𝑣 ) )
41 simpl ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → 𝜑 )
42 3 swopolem ( ( 𝜑 ∧ ( 𝑢𝑋𝑤𝑋𝑣𝑋 ) ) → ( 𝑢 < 𝑤 → ( 𝑢 < 𝑣𝑣 < 𝑤 ) ) )
43 41 29 37 31 42 syl13anc ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ( 𝑢 < 𝑤 → ( 𝑢 < 𝑣𝑣 < 𝑤 ) ) )
44 3 swopolem ( ( 𝜑 ∧ ( 𝑤𝑋𝑢𝑋𝑣𝑋 ) ) → ( 𝑤 < 𝑢 → ( 𝑤 < 𝑣𝑣 < 𝑢 ) ) )
45 41 37 29 31 44 syl13anc ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ( 𝑤 < 𝑢 → ( 𝑤 < 𝑣𝑣 < 𝑢 ) ) )
46 orcom ( ( 𝑣 < 𝑢𝑤 < 𝑣 ) ↔ ( 𝑤 < 𝑣𝑣 < 𝑢 ) )
47 45 46 syl6ibr ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ( 𝑤 < 𝑢 → ( 𝑣 < 𝑢𝑤 < 𝑣 ) ) )
48 43 47 orim12d ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ( ( 𝑢 < 𝑤𝑤 < 𝑢 ) → ( ( 𝑢 < 𝑣𝑣 < 𝑤 ) ∨ ( 𝑣 < 𝑢𝑤 < 𝑣 ) ) ) )
49 or4 ( ( ( 𝑢 < 𝑣𝑣 < 𝑤 ) ∨ ( 𝑣 < 𝑢𝑤 < 𝑣 ) ) ↔ ( ( 𝑢 < 𝑣𝑣 < 𝑢 ) ∨ ( 𝑣 < 𝑤𝑤 < 𝑣 ) ) )
50 48 49 syl6ib ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ( ( 𝑢 < 𝑤𝑤 < 𝑢 ) → ( ( 𝑢 < 𝑣𝑣 < 𝑢 ) ∨ ( 𝑣 < 𝑤𝑤 < 𝑣 ) ) ) )
51 33 40 50 mtord ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ¬ ( 𝑢 < 𝑤𝑤 < 𝑢 ) )
52 1 brdifun ( ( 𝑢𝑋𝑤𝑋 ) → ( 𝑢 𝑅 𝑤 ↔ ¬ ( 𝑢 < 𝑤𝑤 < 𝑢 ) ) )
53 29 37 52 syl2anc ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → ( 𝑢 𝑅 𝑤 ↔ ¬ ( 𝑢 < 𝑤𝑤 < 𝑢 ) ) )
54 51 53 mpbird ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣𝑣 𝑅 𝑤 ) ) → 𝑢 𝑅 𝑤 )
55 2 3 swopo ( 𝜑< Po 𝑋 )
56 poirr ( ( < Po 𝑋𝑢𝑋 ) → ¬ 𝑢 < 𝑢 )
57 55 56 sylan ( ( 𝜑𝑢𝑋 ) → ¬ 𝑢 < 𝑢 )
58 pm1.2 ( ( 𝑢 < 𝑢𝑢 < 𝑢 ) → 𝑢 < 𝑢 )
59 57 58 nsyl ( ( 𝜑𝑢𝑋 ) → ¬ ( 𝑢 < 𝑢𝑢 < 𝑢 ) )
60 simpr ( ( 𝜑𝑢𝑋 ) → 𝑢𝑋 )
61 1 brdifun ( ( 𝑢𝑋𝑢𝑋 ) → ( 𝑢 𝑅 𝑢 ↔ ¬ ( 𝑢 < 𝑢𝑢 < 𝑢 ) ) )
62 60 60 61 syl2anc ( ( 𝜑𝑢𝑋 ) → ( 𝑢 𝑅 𝑢 ↔ ¬ ( 𝑢 < 𝑢𝑢 < 𝑢 ) ) )
63 59 62 mpbird ( ( 𝜑𝑢𝑋 ) → 𝑢 𝑅 𝑢 )
64 5 ssbri ( 𝑢 𝑅 𝑢𝑢 ( 𝑋 × 𝑋 ) 𝑢 )
65 brxp ( 𝑢 ( 𝑋 × 𝑋 ) 𝑢 ↔ ( 𝑢𝑋𝑢𝑋 ) )
66 65 simplbi ( 𝑢 ( 𝑋 × 𝑋 ) 𝑢𝑢𝑋 )
67 64 66 syl ( 𝑢 𝑅 𝑢𝑢𝑋 )
68 67 adantl ( ( 𝜑𝑢 𝑅 𝑢 ) → 𝑢𝑋 )
69 63 68 impbida ( 𝜑 → ( 𝑢𝑋𝑢 𝑅 𝑢 ) )
70 9 25 54 69 iserd ( 𝜑𝑅 Er 𝑋 )