Step | Hyp | Ref
| Expression |
1 | | poinxp 4352 |
. . 3
⊢ (𝑅 Po A ↔ (𝑅 ∩ (A × A)) Po
A) |
2 | | brinxp 4351 |
. . . . . . . 8
⊢
((x ∈ A ∧ y ∈ A) →
(x𝑅y ↔
x(𝑅 ∩ (A × A))y)) |
3 | 2 | 3adant3 923 |
. . . . . . 7
⊢
((x ∈ A ∧ y ∈ A ∧ z ∈ A) →
(x𝑅y ↔
x(𝑅 ∩ (A × A))y)) |
4 | | brinxp 4351 |
. . . . . . . . 9
⊢
((x ∈ A ∧ z ∈ A) →
(x𝑅z ↔
x(𝑅 ∩ (A × A))z)) |
5 | 4 | 3adant2 922 |
. . . . . . . 8
⊢
((x ∈ A ∧ y ∈ A ∧ z ∈ A) →
(x𝑅z ↔
x(𝑅 ∩ (A × A))z)) |
6 | | brinxp 4351 |
. . . . . . . . . 10
⊢
((z ∈ A ∧ y ∈ A) →
(z𝑅y ↔
z(𝑅 ∩ (A × A))y)) |
7 | 6 | ancoms 255 |
. . . . . . . . 9
⊢
((y ∈ A ∧ z ∈ A) →
(z𝑅y ↔
z(𝑅 ∩ (A × A))y)) |
8 | 7 | 3adant1 921 |
. . . . . . . 8
⊢
((x ∈ A ∧ y ∈ A ∧ z ∈ A) →
(z𝑅y ↔
z(𝑅 ∩ (A × A))y)) |
9 | 5, 8 | orbi12d 706 |
. . . . . . 7
⊢
((x ∈ A ∧ y ∈ A ∧ z ∈ A) →
((x𝑅z ∨ z𝑅y) ↔ (x(𝑅 ∩ (A × A))z ∨ z(𝑅 ∩ (A × A))y))) |
10 | 3, 9 | imbi12d 223 |
. . . . . 6
⊢
((x ∈ A ∧ y ∈ A ∧ z ∈ A) →
((x𝑅y →
(x𝑅z ∨ z𝑅y)) ↔ (x(𝑅 ∩ (A × A))y →
(x(𝑅 ∩ (A × A))z ∨ z(𝑅 ∩ (A × A))y)))) |
11 | 10 | 3expb 1104 |
. . . . 5
⊢
((x ∈ A ∧ (y ∈ A ∧ z ∈ A)) →
((x𝑅y →
(x𝑅z ∨ z𝑅y)) ↔ (x(𝑅 ∩ (A × A))y →
(x(𝑅 ∩ (A × A))z ∨ z(𝑅 ∩ (A × A))y)))) |
12 | 11 | 2ralbidva 2340 |
. . . 4
⊢ (x ∈ A → (∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) ↔ ∀y ∈ A ∀z ∈ A (x(𝑅 ∩ (A × A))y →
(x(𝑅 ∩ (A × A))z ∨ z(𝑅 ∩ (A × A))y)))) |
13 | 12 | ralbiia 2332 |
. . 3
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x(𝑅 ∩ (A × A))y →
(x(𝑅 ∩ (A × A))z ∨ z(𝑅 ∩ (A × A))y))) |
14 | 1, 13 | anbi12i 433 |
. 2
⊢ ((𝑅 Po A ∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y))) ↔ ((𝑅 ∩ (A × A)) Po
A ∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x(𝑅 ∩ (A × A))y →
(x(𝑅 ∩ (A × A))z ∨ z(𝑅 ∩ (A × A))y)))) |
15 | | df-iso 4025 |
. 2
⊢ (𝑅 Or A ↔ (𝑅 Po A
∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
16 | | df-iso 4025 |
. 2
⊢ ((𝑅 ∩ (A × A)) Or
A ↔ ((𝑅 ∩ (A × A)) Po
A ∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x(𝑅 ∩ (A × A))y →
(x(𝑅 ∩ (A × A))z ∨ z(𝑅 ∩ (A × A))y)))) |
17 | 14, 15, 16 | 3bitr4i 201 |
1
⊢ (𝑅 Or A ↔ (𝑅 ∩ (A × A)) Or
A) |