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

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 imbitrrdi ⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( 𝑤 < 𝑢 → ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ) )
48 43 47 orim12d ⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) → ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ∨ ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ) ) )
49 or4 ⊢ ( ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑤 ) ∨ ( 𝑣 < 𝑢 ∨ 𝑤 < 𝑣 ) ) ↔ ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ∨ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) )
50 48 49 imbitrdi ⊢ ( ( 𝜑 ∧ ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ) → ( ( 𝑢 < 𝑤 ∨ 𝑤 < 𝑢 ) → ( ( 𝑢 < 𝑣 ∨ 𝑣 < 𝑢 ) ∨ ( 𝑣 < 𝑤 ∨ 𝑤 < 𝑣 ) ) ) )
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 𝑋 )