Proof of Theorem sotritrieq
Step | Hyp | Ref
| Expression |
1 | | sotritric.or |
. . . . . . 7
⊢ 𝑅 Or 𝐴 |
2 | | sonr 4300 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
3 | 1, 2 | mpan 422 |
. . . . . 6
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐵𝑅𝐵) |
4 | | breq2 3991 |
. . . . . . 7
⊢ (𝐵 = 𝐶 → (𝐵𝑅𝐵 ↔ 𝐵𝑅𝐶)) |
5 | 4 | notbid 662 |
. . . . . 6
⊢ (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐵𝑅𝐶)) |
6 | 3, 5 | syl5ibcom 154 |
. . . . 5
⊢ (𝐵 ∈ 𝐴 → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶)) |
7 | | breq1 3990 |
. . . . . . 7
⊢ (𝐵 = 𝐶 → (𝐵𝑅𝐵 ↔ 𝐶𝑅𝐵)) |
8 | 7 | notbid 662 |
. . . . . 6
⊢ (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐶𝑅𝐵)) |
9 | 3, 8 | syl5ibcom 154 |
. . . . 5
⊢ (𝐵 ∈ 𝐴 → (𝐵 = 𝐶 → ¬ 𝐶𝑅𝐵)) |
10 | 6, 9 | jcad 305 |
. . . 4
⊢ (𝐵 ∈ 𝐴 → (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐶 ∧ ¬ 𝐶𝑅𝐵))) |
11 | | ioran 747 |
. . . 4
⊢ (¬
(𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵) ↔ (¬ 𝐵𝑅𝐶 ∧ ¬ 𝐶𝑅𝐵)) |
12 | 10, 11 | syl6ibr 161 |
. . 3
⊢ (𝐵 ∈ 𝐴 → (𝐵 = 𝐶 → ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) |
13 | 12 | adantr 274 |
. 2
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵 = 𝐶 → ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) |
14 | | sotritric.tri |
. . 3
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) |
15 | | 3orrot 979 |
. . . . . . 7
⊢ ((𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) ↔ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵 ∨ 𝐵𝑅𝐶)) |
16 | | 3orcomb 982 |
. . . . . . 7
⊢ ((𝐵 = 𝐶 ∨ 𝐶𝑅𝐵 ∨ 𝐵𝑅𝐶) ↔ (𝐵 = 𝐶 ∨ 𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵)) |
17 | | 3orass 976 |
. . . . . . 7
⊢ ((𝐵 = 𝐶 ∨ 𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵) ↔ (𝐵 = 𝐶 ∨ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) |
18 | 15, 16, 17 | 3bitri 205 |
. . . . . 6
⊢ ((𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) ↔ (𝐵 = 𝐶 ∨ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) |
19 | 18 | biimpi 119 |
. . . . 5
⊢ ((𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) → (𝐵 = 𝐶 ∨ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) |
20 | 19 | orcomd 724 |
. . . 4
⊢ ((𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) → ((𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵) ∨ 𝐵 = 𝐶)) |
21 | 20 | ord 719 |
. . 3
⊢ ((𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) → (¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵) → 𝐵 = 𝐶)) |
22 | 14, 21 | syl 14 |
. 2
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵) → 𝐵 = 𝐶)) |
23 | 13, 22 | impbid 128 |
1
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) |