Step |
Hyp |
Ref |
Expression |
1 |
|
breq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 𝑅 𝑦 ↔ 𝐵 𝑅 𝑦 ) ) |
2 |
|
eqeq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝑦 ↔ 𝐵 = 𝑦 ) ) |
3 |
|
breq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐵 ) ) |
4 |
1 2 3
|
3orbi123d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝐵 𝑅 𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦 𝑅 𝐵 ) ) ) |
5 |
4
|
imbi2d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝑅 Or 𝐴 → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ↔ ( 𝑅 Or 𝐴 → ( 𝐵 𝑅 𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦 𝑅 𝐵 ) ) ) ) |
6 |
|
breq2 |
⊢ ( 𝑦 = 𝐶 → ( 𝐵 𝑅 𝑦 ↔ 𝐵 𝑅 𝐶 ) ) |
7 |
|
eqeq2 |
⊢ ( 𝑦 = 𝐶 → ( 𝐵 = 𝑦 ↔ 𝐵 = 𝐶 ) ) |
8 |
|
breq1 |
⊢ ( 𝑦 = 𝐶 → ( 𝑦 𝑅 𝐵 ↔ 𝐶 𝑅 𝐵 ) ) |
9 |
6 7 8
|
3orbi123d |
⊢ ( 𝑦 = 𝐶 → ( ( 𝐵 𝑅 𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦 𝑅 𝐵 ) ↔ ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) ) |
10 |
9
|
imbi2d |
⊢ ( 𝑦 = 𝐶 → ( ( 𝑅 Or 𝐴 → ( 𝐵 𝑅 𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦 𝑅 𝐵 ) ) ↔ ( 𝑅 Or 𝐴 → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) ) ) |
11 |
|
df-so |
⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ) |
12 |
|
rsp2 |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ) |
13 |
11 12
|
simplbiim |
⊢ ( 𝑅 Or 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ) |
14 |
13
|
com12 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑅 Or 𝐴 → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ) |
15 |
5 10 14
|
vtocl2ga |
⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑅 Or 𝐴 → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) ) |
16 |
15
|
impcom |
⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 𝑅 𝐵 ) ) |