Detailed syntax breakdown of Definition df-po
| Step | Hyp | Ref
| Expression |
| 1 | | cA |
. . 3
class 𝐴 |
| 2 | | cR |
. . 3
class 𝑅 |
| 3 | 1, 2 | wpo 5590 |
. 2
wff 𝑅 Po 𝐴 |
| 4 | | vx |
. . . . . . . . 9
setvar 𝑥 |
| 5 | 4 | cv 1539 |
. . . . . . . 8
class 𝑥 |
| 6 | 5, 5, 2 | wbr 5143 |
. . . . . . 7
wff 𝑥𝑅𝑥 |
| 7 | 6 | wn 3 |
. . . . . 6
wff ¬
𝑥𝑅𝑥 |
| 8 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
| 9 | 8 | cv 1539 |
. . . . . . . . 9
class 𝑦 |
| 10 | 5, 9, 2 | wbr 5143 |
. . . . . . . 8
wff 𝑥𝑅𝑦 |
| 11 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
| 12 | 11 | cv 1539 |
. . . . . . . . 9
class 𝑧 |
| 13 | 9, 12, 2 | wbr 5143 |
. . . . . . . 8
wff 𝑦𝑅𝑧 |
| 14 | 10, 13 | wa 395 |
. . . . . . 7
wff (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) |
| 15 | 5, 12, 2 | wbr 5143 |
. . . . . . 7
wff 𝑥𝑅𝑧 |
| 16 | 14, 15 | wi 4 |
. . . . . 6
wff ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) |
| 17 | 7, 16 | wa 395 |
. . . . 5
wff (¬
𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
| 18 | 17, 11, 1 | wral 3061 |
. . . 4
wff
∀𝑧 ∈
𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
| 19 | 18, 8, 1 | wral 3061 |
. . 3
wff
∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
| 20 | 19, 4, 1 | wral 3061 |
. 2
wff
∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
| 21 | 3, 20 | wb 206 |
1
wff (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |