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 ⊢ 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ◡ < ) )
swoer.2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 < 𝑧 → ¬ 𝑧 < 𝑦 ) )
swoer.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 < 𝑦 → ( 𝑥 < 𝑧 ∨ 𝑧 < 𝑦 ) ) )
swoord.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
swoord.5 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
swoord.6 ⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
Assertion swoord1 ( 𝜑 → ( 𝐴 < 𝐶 ↔ 𝐵 < 𝐶 ) )

Proof

Step Hyp Ref Expression
1 swoer.1 ⊢ 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ◡ < ) )
2 swoer.2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 < 𝑧 → ¬ 𝑧 < 𝑦 ) )
3 swoer.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 < 𝑦 → ( 𝑥 < 𝑧 ∨ 𝑧 < 𝑦 ) ) )
4 swoord.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
5 swoord.5 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
6 swoord.6 ⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
7 id ⊢ ( 𝜑 → 𝜑 )
8 difss ⊢ ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ◡ < ) ) ⊆ ( 𝑋 × 𝑋 )
9 1 8 eqsstri ⊢ 𝑅 ⊆ ( 𝑋 × 𝑋 )
10 9 ssbri ⊢ ( 𝐴 𝑅 𝐵 → 𝐴 ( 𝑋 × 𝑋 ) 𝐵 )
11 df-br ⊢ ( 𝐴 ( 𝑋 × 𝑋 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) )
12 opelxp1 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) → 𝐴 ∈ 𝑋 )
13 11 12 sylbi ⊢ ( 𝐴 ( 𝑋 × 𝑋 ) 𝐵 → 𝐴 ∈ 𝑋 )
14 6 10 13 3syl ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
15 3 swopolem ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 < 𝐶 → ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐶 ) ) )
16 7 14 5 4 15 syl13anc ⊢ ( 𝜑 → ( 𝐴 < 𝐶 → ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐶 ) ) )
17 1 brdifun ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ↔ ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
18 14 4 17 syl2anc ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
19 6 18 mpbid ⊢ ( 𝜑 → ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) )
20 orc ⊢ ( 𝐴 < 𝐵 → ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) )
21 19 20 nsyl ⊢ ( 𝜑 → ¬ 𝐴 < 𝐵 )
22 biorf ⊢ ( ¬ 𝐴 < 𝐵 → ( 𝐵 < 𝐶 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐶 ) ) )
23 21 22 syl ⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐶 ) ) )
24 16 23 sylibrd ⊢ ( 𝜑 → ( 𝐴 < 𝐶 → 𝐵 < 𝐶 ) )
25 3 swopolem ⊢ ( ( 𝜑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐵 < 𝐶 → ( 𝐵 < 𝐴 ∨ 𝐴 < 𝐶 ) ) )
26 7 4 5 14 25 syl13anc ⊢ ( 𝜑 → ( 𝐵 < 𝐶 → ( 𝐵 < 𝐴 ∨ 𝐴 < 𝐶 ) ) )
27 olc ⊢ ( 𝐵 < 𝐴 → ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) )
28 19 27 nsyl ⊢ ( 𝜑 → ¬ 𝐵 < 𝐴 )
29 biorf ⊢ ( ¬ 𝐵 < 𝐴 → ( 𝐴 < 𝐶 ↔ ( 𝐵 < 𝐴 ∨ 𝐴 < 𝐶 ) ) )
30 28 29 syl ⊢ ( 𝜑 → ( 𝐴 < 𝐶 ↔ ( 𝐵 < 𝐴 ∨ 𝐴 < 𝐶 ) ) )
31 26 30 sylibrd ⊢ ( 𝜑 → ( 𝐵 < 𝐶 → 𝐴 < 𝐶 ) )
32 24 31 impbid ⊢ ( 𝜑 → ( 𝐴 < 𝐶 ↔ 𝐵 < 𝐶 ) )