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

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

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 5 14 4 15 syl13anc ⊢ ( 𝜑 → ( 𝐶 < 𝐴 → ( 𝐶 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
17 idd ⊢ ( 𝜑 → ( 𝐶 < 𝐵 → 𝐶 < 𝐵 ) )
18 1 brdifun ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ↔ ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
19 14 4 18 syl2anc ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
20 6 19 mpbid ⊢ ( 𝜑 → ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) )
21 olc ⊢ ( 𝐵 < 𝐴 → ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) )
22 20 21 nsyl ⊢ ( 𝜑 → ¬ 𝐵 < 𝐴 )
23 22 pm2.21d ⊢ ( 𝜑 → ( 𝐵 < 𝐴 → 𝐶 < 𝐵 ) )
24 17 23 jaod ⊢ ( 𝜑 → ( ( 𝐶 < 𝐵 ∨ 𝐵 < 𝐴 ) → 𝐶 < 𝐵 ) )
25 16 24 syld ⊢ ( 𝜑 → ( 𝐶 < 𝐴 → 𝐶 < 𝐵 ) )
26 3 swopolem ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐶 < 𝐵 → ( 𝐶 < 𝐴 ∨ 𝐴 < 𝐵 ) ) )
27 7 5 4 14 26 syl13anc ⊢ ( 𝜑 → ( 𝐶 < 𝐵 → ( 𝐶 < 𝐴 ∨ 𝐴 < 𝐵 ) ) )
28 idd ⊢ ( 𝜑 → ( 𝐶 < 𝐴 → 𝐶 < 𝐴 ) )
29 orc ⊢ ( 𝐴 < 𝐵 → ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) )
30 20 29 nsyl ⊢ ( 𝜑 → ¬ 𝐴 < 𝐵 )
31 30 pm2.21d ⊢ ( 𝜑 → ( 𝐴 < 𝐵 → 𝐶 < 𝐴 ) )
32 28 31 jaod ⊢ ( 𝜑 → ( ( 𝐶 < 𝐴 ∨ 𝐴 < 𝐵 ) → 𝐶 < 𝐴 ) )
33 27 32 syld ⊢ ( 𝜑 → ( 𝐶 < 𝐵 → 𝐶 < 𝐴 ) )
34 25 33 impbid ⊢ ( 𝜑 → ( 𝐶 < 𝐴 ↔ 𝐶 < 𝐵 ) )