Proof of Theorem swoord2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . 4
⊢ (𝜑 → 𝜑) | 
| 2 |  | swoord.5 | . . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑋) | 
| 3 |  | swoord.6 | . . . . 5
⊢ (𝜑 → 𝐴𝑅𝐵) | 
| 4 |  | swoer.1 | . . . . . . 7
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) | 
| 5 |  | difss 4135 | . . . . . . 7
⊢ ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) ⊆ (𝑋 × 𝑋) | 
| 6 | 4, 5 | eqsstri 4029 | . . . . . 6
⊢ 𝑅 ⊆ (𝑋 × 𝑋) | 
| 7 | 6 | ssbri 5187 | . . . . 5
⊢ (𝐴𝑅𝐵 → 𝐴(𝑋 × 𝑋)𝐵) | 
| 8 |  | df-br 5143 | . . . . . 6
⊢ (𝐴(𝑋 × 𝑋)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑋)) | 
| 9 |  | opelxp1 5726 | . . . . . 6
⊢
(〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑋) → 𝐴 ∈ 𝑋) | 
| 10 | 8, 9 | sylbi 217 | . . . . 5
⊢ (𝐴(𝑋 × 𝑋)𝐵 → 𝐴 ∈ 𝑋) | 
| 11 | 3, 7, 10 | 3syl 18 | . . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑋) | 
| 12 |  | swoord.4 | . . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑋) | 
| 13 |  | swoer.3 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) | 
| 14 | 13 | swopolem 5601 | . . . 4
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐶 < 𝐴 → (𝐶 < 𝐵 ∨ 𝐵 < 𝐴))) | 
| 15 | 1, 2, 11, 12, 14 | syl13anc 1373 | . . 3
⊢ (𝜑 → (𝐶 < 𝐴 → (𝐶 < 𝐵 ∨ 𝐵 < 𝐴))) | 
| 16 |  | idd 24 | . . . 4
⊢ (𝜑 → (𝐶 < 𝐵 → 𝐶 < 𝐵)) | 
| 17 | 4 | brdifun 8776 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | 
| 18 | 11, 12, 17 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | 
| 19 | 3, 18 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) | 
| 20 |  | olc 868 | . . . . . 6
⊢ (𝐵 < 𝐴 → (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) | 
| 21 | 19, 20 | nsyl 140 | . . . . 5
⊢ (𝜑 → ¬ 𝐵 < 𝐴) | 
| 22 | 21 | pm2.21d 121 | . . . 4
⊢ (𝜑 → (𝐵 < 𝐴 → 𝐶 < 𝐵)) | 
| 23 | 16, 22 | jaod 859 | . . 3
⊢ (𝜑 → ((𝐶 < 𝐵 ∨ 𝐵 < 𝐴) → 𝐶 < 𝐵)) | 
| 24 | 15, 23 | syld 47 | . 2
⊢ (𝜑 → (𝐶 < 𝐴 → 𝐶 < 𝐵)) | 
| 25 | 13 | swopolem 5601 | . . . 4
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐶 < 𝐵 → (𝐶 < 𝐴 ∨ 𝐴 < 𝐵))) | 
| 26 | 1, 2, 12, 11, 25 | syl13anc 1373 | . . 3
⊢ (𝜑 → (𝐶 < 𝐵 → (𝐶 < 𝐴 ∨ 𝐴 < 𝐵))) | 
| 27 |  | idd 24 | . . . 4
⊢ (𝜑 → (𝐶 < 𝐴 → 𝐶 < 𝐴)) | 
| 28 |  | orc 867 | . . . . . 6
⊢ (𝐴 < 𝐵 → (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) | 
| 29 | 19, 28 | nsyl 140 | . . . . 5
⊢ (𝜑 → ¬ 𝐴 < 𝐵) | 
| 30 | 29 | pm2.21d 121 | . . . 4
⊢ (𝜑 → (𝐴 < 𝐵 → 𝐶 < 𝐴)) | 
| 31 | 27, 30 | jaod 859 | . . 3
⊢ (𝜑 → ((𝐶 < 𝐴 ∨ 𝐴 < 𝐵) → 𝐶 < 𝐴)) | 
| 32 | 26, 31 | syld 47 | . 2
⊢ (𝜑 → (𝐶 < 𝐵 → 𝐶 < 𝐴)) | 
| 33 | 24, 32 | impbid 212 | 1
⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) |