Detailed syntax breakdown of Definition df-iso
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class A |
2 | | cR |
. . 3
class 𝑅 |
3 | 1, 2 | wor 4023 |
. 2
wff 𝑅 Or A |
4 | 1, 2 | wpo 4022 |
. . 3
wff 𝑅 Po A |
5 | | vx |
. . . . . . . . 9
setvar x |
6 | 5 | cv 1241 |
. . . . . . . 8
class x |
7 | | vy |
. . . . . . . . 9
setvar y |
8 | 7 | cv 1241 |
. . . . . . . 8
class y |
9 | 6, 8, 2 | wbr 3755 |
. . . . . . 7
wff x𝑅y |
10 | | vz |
. . . . . . . . . 10
setvar z |
11 | 10 | cv 1241 |
. . . . . . . . 9
class z |
12 | 6, 11, 2 | wbr 3755 |
. . . . . . . 8
wff x𝑅z |
13 | 11, 8, 2 | wbr 3755 |
. . . . . . . 8
wff z𝑅y |
14 | 12, 13 | wo 628 |
. . . . . . 7
wff (x𝑅z ∨ z𝑅y) |
15 | 9, 14 | wi 4 |
. . . . . 6
wff (x𝑅y →
(x𝑅z ∨ z𝑅y)) |
16 | 15, 10, 1 | wral 2300 |
. . . . 5
wff ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) |
17 | 16, 7, 1 | wral 2300 |
. . . 4
wff ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) |
18 | 17, 5, 1 | wral 2300 |
. . 3
wff ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) |
19 | 4, 18 | wa 97 |
. 2
wff (𝑅 Po A
∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y))) |
20 | 3, 19 | wb 98 |
1
wff (𝑅 Or A
↔ (𝑅 Po A ∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)))) |