Proof of Theorem swoord2
Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . 4
⊢ (𝜑 → 𝜑) |
2 | | swoord.5 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
3 | | swoord.6 |
. . . . 5
⊢ (𝜑 → 𝐴𝑅𝐵) |
4 | | swoer.1 |
. . . . . . 7
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) |
5 | | difss 3234 |
. . . . . . 7
⊢ ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) ⊆ (𝑋 × 𝑋) |
6 | 4, 5 | eqsstri 3160 |
. . . . . 6
⊢ 𝑅 ⊆ (𝑋 × 𝑋) |
7 | 6 | ssbri 4010 |
. . . . 5
⊢ (𝐴𝑅𝐵 → 𝐴(𝑋 × 𝑋)𝐵) |
8 | | df-br 3968 |
. . . . . 6
⊢ (𝐴(𝑋 × 𝑋)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑋)) |
9 | | opelxp1 4622 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑋) → 𝐴 ∈ 𝑋) |
10 | 8, 9 | sylbi 120 |
. . . . 5
⊢ (𝐴(𝑋 × 𝑋)𝐵 → 𝐴 ∈ 𝑋) |
11 | 3, 7, 10 | 3syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
12 | | swoord.4 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑋) |
13 | | swoer.3 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) |
14 | 13 | swopolem 4267 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐶 < 𝐴 → (𝐶 < 𝐵 ∨ 𝐵 < 𝐴))) |
15 | 1, 2, 11, 12, 14 | syl13anc 1222 |
. . 3
⊢ (𝜑 → (𝐶 < 𝐴 → (𝐶 < 𝐵 ∨ 𝐵 < 𝐴))) |
16 | | idd 21 |
. . . 4
⊢ (𝜑 → (𝐶 < 𝐵 → 𝐶 < 𝐵)) |
17 | 4 | brdifun 6509 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) |
18 | 11, 12, 17 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) |
19 | 3, 18 | mpbid 146 |
. . . . . 6
⊢ (𝜑 → ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) |
20 | | olc 701 |
. . . . . 6
⊢ (𝐵 < 𝐴 → (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) |
21 | 19, 20 | nsyl 618 |
. . . . 5
⊢ (𝜑 → ¬ 𝐵 < 𝐴) |
22 | 21 | pm2.21d 609 |
. . . 4
⊢ (𝜑 → (𝐵 < 𝐴 → 𝐶 < 𝐵)) |
23 | 16, 22 | jaod 707 |
. . 3
⊢ (𝜑 → ((𝐶 < 𝐵 ∨ 𝐵 < 𝐴) → 𝐶 < 𝐵)) |
24 | 15, 23 | syld 45 |
. 2
⊢ (𝜑 → (𝐶 < 𝐴 → 𝐶 < 𝐵)) |
25 | 13 | swopolem 4267 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐶 < 𝐵 → (𝐶 < 𝐴 ∨ 𝐴 < 𝐵))) |
26 | 1, 2, 12, 11, 25 | syl13anc 1222 |
. . 3
⊢ (𝜑 → (𝐶 < 𝐵 → (𝐶 < 𝐴 ∨ 𝐴 < 𝐵))) |
27 | | idd 21 |
. . . 4
⊢ (𝜑 → (𝐶 < 𝐴 → 𝐶 < 𝐴)) |
28 | | orc 702 |
. . . . . 6
⊢ (𝐴 < 𝐵 → (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) |
29 | 19, 28 | nsyl 618 |
. . . . 5
⊢ (𝜑 → ¬ 𝐴 < 𝐵) |
30 | 29 | pm2.21d 609 |
. . . 4
⊢ (𝜑 → (𝐴 < 𝐵 → 𝐶 < 𝐴)) |
31 | 27, 30 | jaod 707 |
. . 3
⊢ (𝜑 → ((𝐶 < 𝐴 ∨ 𝐴 < 𝐵) → 𝐶 < 𝐴)) |
32 | 26, 31 | syld 45 |
. 2
⊢ (𝜑 → (𝐶 < 𝐵 → 𝐶 < 𝐴)) |
33 | 24, 32 | impbid 128 |
1
⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) |