Proof of Theorem sotritrieq
Step | Hyp | Ref
| Expression |
1 | | sotritric.or |
. . . . . . 7
⊢ 𝑅 Or A |
2 | | sonr 4045 |
. . . . . . 7
⊢ ((𝑅 Or A ∧ B ∈ A) → ¬ B𝑅B) |
3 | 1, 2 | mpan 400 |
. . . . . 6
⊢ (B ∈ A → ¬ B𝑅B) |
4 | | breq2 3759 |
. . . . . . 7
⊢ (B = 𝐶 → (B𝑅B ↔
B𝑅𝐶)) |
5 | 4 | notbid 591 |
. . . . . 6
⊢ (B = 𝐶 → (¬ B𝑅B ↔
¬ B𝑅𝐶)) |
6 | 3, 5 | syl5ibcom 144 |
. . . . 5
⊢ (B ∈ A → (B =
𝐶 → ¬ B𝑅𝐶)) |
7 | | breq1 3758 |
. . . . . . 7
⊢ (B = 𝐶 → (B𝑅B ↔
𝐶𝑅B)) |
8 | 7 | notbid 591 |
. . . . . 6
⊢ (B = 𝐶 → (¬ B𝑅B ↔
¬ 𝐶𝑅B)) |
9 | 3, 8 | syl5ibcom 144 |
. . . . 5
⊢ (B ∈ A → (B =
𝐶 → ¬ 𝐶𝑅B)) |
10 | 6, 9 | jcad 291 |
. . . 4
⊢ (B ∈ A → (B =
𝐶 → (¬ B𝑅𝐶 ∧ ¬
𝐶𝑅B))) |
11 | | ioran 668 |
. . . 4
⊢ (¬
(B𝑅𝐶 ∨ 𝐶𝑅B)
↔ (¬ B𝑅𝐶 ∧ ¬
𝐶𝑅B)) |
12 | 10, 11 | syl6ibr 151 |
. . 3
⊢ (B ∈ A → (B =
𝐶 → ¬ (B𝑅𝐶 ∨ 𝐶𝑅B))) |
13 | 12 | adantr 261 |
. 2
⊢
((B ∈ A ∧ 𝐶 ∈
A) → (B = 𝐶 → ¬ (B𝑅𝐶 ∨ 𝐶𝑅B))) |
14 | | sotritric.tri |
. . 3
⊢
((B ∈ A ∧ 𝐶 ∈
A) → (B𝑅𝐶 ∨ B = 𝐶 ∨ 𝐶𝑅B)) |
15 | | 3orrot 890 |
. . . . . . 7
⊢
((B𝑅𝐶 ∨ B = 𝐶 ∨ 𝐶𝑅B)
↔ (B = 𝐶 ∨ 𝐶𝑅B ∨ B𝑅𝐶)) |
16 | | 3orcomb 893 |
. . . . . . 7
⊢
((B = 𝐶 ∨ 𝐶𝑅B ∨ B𝑅𝐶) ↔ (B = 𝐶 ∨ B𝑅𝐶 ∨ 𝐶𝑅B)) |
17 | | 3orass 887 |
. . . . . . 7
⊢
((B = 𝐶 ∨ B𝑅𝐶 ∨ 𝐶𝑅B)
↔ (B = 𝐶 ∨
(B𝑅𝐶 ∨ 𝐶𝑅B))) |
18 | 15, 16, 17 | 3bitri 195 |
. . . . . 6
⊢
((B𝑅𝐶 ∨ B = 𝐶 ∨ 𝐶𝑅B)
↔ (B = 𝐶 ∨
(B𝑅𝐶 ∨ 𝐶𝑅B))) |
19 | 18 | biimpi 113 |
. . . . 5
⊢
((B𝑅𝐶 ∨ B = 𝐶 ∨ 𝐶𝑅B)
→ (B = 𝐶 ∨
(B𝑅𝐶 ∨ 𝐶𝑅B))) |
20 | 19 | orcomd 647 |
. . . 4
⊢
((B𝑅𝐶 ∨ B = 𝐶 ∨ 𝐶𝑅B)
→ ((B𝑅𝐶 ∨ 𝐶𝑅B) ∨ B = 𝐶)) |
21 | 20 | ord 642 |
. . 3
⊢
((B𝑅𝐶 ∨ B = 𝐶 ∨ 𝐶𝑅B)
→ (¬ (B𝑅𝐶 ∨ 𝐶𝑅B)
→ B = 𝐶)) |
22 | 14, 21 | syl 14 |
. 2
⊢
((B ∈ A ∧ 𝐶 ∈
A) → (¬ (B𝑅𝐶 ∨ 𝐶𝑅B)
→ B = 𝐶)) |
23 | 13, 22 | impbid 120 |
1
⊢
((B ∈ A ∧ 𝐶 ∈
A) → (B = 𝐶 ↔ ¬ (B𝑅𝐶 ∨ 𝐶𝑅B))) |