Step | Hyp | Ref
| Expression |
1 | | breq1 3758 |
. . . . 5
⊢ (x = B →
(x𝑅y ↔
B𝑅y)) |
2 | | breq1 3758 |
. . . . . 6
⊢ (x = B →
(x𝑅z ↔
B𝑅z)) |
3 | 2 | orbi1d 704 |
. . . . 5
⊢ (x = B →
((x𝑅z ∨ z𝑅y) ↔ (B𝑅z ∨ z𝑅y))) |
4 | 1, 3 | imbi12d 223 |
. . . 4
⊢ (x = B →
((x𝑅y →
(x𝑅z ∨ z𝑅y)) ↔ (B𝑅y →
(B𝑅z ∨ z𝑅y)))) |
5 | 4 | imbi2d 219 |
. . 3
⊢ (x = B →
((𝑅 Or A → (x𝑅y → (x𝑅z ∨ z𝑅y)))
↔ (𝑅 Or A → (B𝑅y → (B𝑅z ∨ z𝑅y))))) |
6 | | breq2 3759 |
. . . . 5
⊢ (y = 𝐶 → (B𝑅y ↔
B𝑅𝐶)) |
7 | | breq2 3759 |
. . . . . 6
⊢ (y = 𝐶 → (z𝑅y ↔
z𝑅𝐶)) |
8 | 7 | orbi2d 703 |
. . . . 5
⊢ (y = 𝐶 → ((B𝑅z ∨ z𝑅y) ↔ (B𝑅z ∨ z𝑅𝐶))) |
9 | 6, 8 | imbi12d 223 |
. . . 4
⊢ (y = 𝐶 → ((B𝑅y →
(B𝑅z ∨ z𝑅y)) ↔ (B𝑅𝐶 → (B𝑅z ∨ z𝑅𝐶)))) |
10 | 9 | imbi2d 219 |
. . 3
⊢ (y = 𝐶 → ((𝑅 Or A
→ (B𝑅y →
(B𝑅z ∨ z𝑅y))) ↔ (𝑅 Or A
→ (B𝑅𝐶 → (B𝑅z ∨ z𝑅𝐶))))) |
11 | | breq2 3759 |
. . . . . 6
⊢ (z = 𝐷 → (B𝑅z ↔
B𝑅𝐷)) |
12 | | breq1 3758 |
. . . . . 6
⊢ (z = 𝐷 → (z𝑅𝐶 ↔ 𝐷𝑅𝐶)) |
13 | 11, 12 | orbi12d 706 |
. . . . 5
⊢ (z = 𝐷 → ((B𝑅z ∨ z𝑅𝐶) ↔ (B𝑅𝐷 ∨ 𝐷𝑅𝐶))) |
14 | 13 | imbi2d 219 |
. . . 4
⊢ (z = 𝐷 → ((B𝑅𝐶 → (B𝑅z ∨ z𝑅𝐶)) ↔ (B𝑅𝐶 → (B𝑅𝐷 ∨ 𝐷𝑅𝐶)))) |
15 | 14 | imbi2d 219 |
. . 3
⊢ (z = 𝐷 → ((𝑅 Or A
→ (B𝑅𝐶 → (B𝑅z ∨ z𝑅𝐶))) ↔ (𝑅 Or A
→ (B𝑅𝐶 → (B𝑅𝐷 ∨ 𝐷𝑅𝐶))))) |
16 | | df-iso 4025 |
. . . . 5
⊢ (𝑅 Or A ↔ (𝑅 Po A
∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
17 | | 3anass 888 |
. . . . . . 7
⊢
((x ∈ A ∧ y ∈ A ∧ z ∈ A) ↔
(x ∈
A ∧
(y ∈
A ∧
z ∈
A))) |
18 | | rsp 2363 |
. . . . . . . . 9
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) → (x
∈ A
→ ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y)))) |
19 | | rsp2 2365 |
. . . . . . . . 9
⊢ (∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) → ((y
∈ A ∧ z ∈ A) →
(x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
20 | 18, 19 | syl6 29 |
. . . . . . . 8
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) → (x
∈ A
→ ((y ∈ A ∧ z ∈ A) →
(x𝑅y →
(x𝑅z ∨ z𝑅y))))) |
21 | 20 | impd 242 |
. . . . . . 7
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) → ((x
∈ A ∧ (y ∈ A ∧ z ∈ A)) →
(x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
22 | 17, 21 | syl5bi 141 |
. . . . . 6
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) → ((x
∈ A ∧ y ∈ A ∧ z ∈ A) →
(x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
23 | 22 | adantl 262 |
. . . . 5
⊢ ((𝑅 Po A ∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y))) → ((x
∈ A ∧ y ∈ A ∧ z ∈ A) →
(x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
24 | 16, 23 | sylbi 114 |
. . . 4
⊢ (𝑅 Or A → ((x
∈ A ∧ y ∈ A ∧ z ∈ A) →
(x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
25 | 24 | com12 27 |
. . 3
⊢
((x ∈ A ∧ y ∈ A ∧ z ∈ A) →
(𝑅 Or A → (x𝑅y → (x𝑅z ∨ z𝑅y)))) |
26 | 5, 10, 15, 25 | vtocl3ga 2617 |
. 2
⊢
((B ∈ A ∧ 𝐶 ∈
A ∧ 𝐷 ∈ A) →
(𝑅 Or A → (B𝑅𝐶 → (B𝑅𝐷 ∨ 𝐷𝑅𝐶)))) |
27 | 26 | impcom 116 |
1
⊢ ((𝑅 Or A ∧ (B ∈ A ∧ 𝐶 ∈ A ∧ 𝐷 ∈
A)) → (B𝑅𝐶 → (B𝑅𝐷 ∨ 𝐷𝑅𝐶))) |