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 ∖ < ˙ ∪ < ˙ -1
swoer.2 ⊢ φ ∧ y ∈ X ∧ z ∈ X → y < ˙ z → ¬ z < ˙ y
swoer.3 ⊢ φ ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X → x < ˙ y → x < ˙ z ∨ z < ˙ y
swoord.4 ⊢ φ → B ∈ X
swoord.5 ⊢ φ → C ∈ X
swoord.6 ⊢ φ → A R B
Assertion swoord2 ⊢ φ → C < ˙ A ↔ C < ˙ B

Proof

Step Hyp Ref Expression
1 swoer.1 ⊢ R = X × X ∖ < ˙ ∪ < ˙ -1
2 swoer.2 ⊢ φ ∧ y ∈ X ∧ z ∈ X → y < ˙ z → ¬ z < ˙ y
3 swoer.3 ⊢ φ ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X → x < ˙ y → x < ˙ z ∨ z < ˙ y
4 swoord.4 ⊢ φ → B ∈ X
5 swoord.5 ⊢ φ → C ∈ X
6 swoord.6 ⊢ φ → A R B
7 id ⊢ φ → φ
8 difss ⊢ X × X ∖ < ˙ ∪ < ˙ -1 ⊆ X × X
9 1 8 eqsstri ⊢ R ⊆ X × X
10 9 ssbri ⊢ A R B → A X × X B
11 df-br ⊢ A X × X B ↔ A B ∈ X × X
12 opelxp1 ⊢ A B ∈ X × X → A ∈ X
13 11 12 sylbi ⊢ A X × X B → A ∈ X
14 6 10 13 3syl ⊢ φ → A ∈ X
15 3 swopolem ⊢ φ ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → C < ˙ A → C < ˙ B ∨ B < ˙ A
16 7 5 14 4 15 syl13anc ⊢ φ → C < ˙ A → C < ˙ B ∨ B < ˙ A
17 idd ⊢ φ → C < ˙ B → C < ˙ B
18 1 brdifun ⊢ A ∈ X ∧ B ∈ X → A R B ↔ ¬ A < ˙ B ∨ B < ˙ A
19 14 4 18 syl2anc ⊢ φ → A R B ↔ ¬ A < ˙ B ∨ B < ˙ A
20 6 19 mpbid ⊢ φ → ¬ A < ˙ B ∨ B < ˙ A
21 olc ⊢ B < ˙ A → A < ˙ B ∨ B < ˙ A
22 20 21 nsyl ⊢ φ → ¬ B < ˙ A
23 22 pm2.21d ⊢ φ → B < ˙ A → C < ˙ B
24 17 23 jaod ⊢ φ → C < ˙ B ∨ B < ˙ A → C < ˙ B
25 16 24 syld ⊢ φ → C < ˙ A → C < ˙ B
26 3 swopolem ⊢ φ ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → C < ˙ B → C < ˙ A ∨ A < ˙ B
27 7 5 4 14 26 syl13anc ⊢ φ → C < ˙ B → C < ˙ A ∨ A < ˙ B
28 idd ⊢ φ → C < ˙ A → C < ˙ A
29 orc ⊢ A < ˙ B → A < ˙ B ∨ B < ˙ A
30 20 29 nsyl ⊢ φ → ¬ A < ˙ B
31 30 pm2.21d ⊢ φ → A < ˙ B → C < ˙ A
32 28 31 jaod ⊢ φ → C < ˙ A ∨ A < ˙ B → C < ˙ A
33 27 32 syld ⊢ φ → C < ˙ B → C < ˙ A
34 25 33 impbid ⊢ φ → C < ˙ A ↔ C < ˙ B