Detailed syntax breakdown of Definition df-tsk
Step | Hyp | Ref
| Expression |
1 | | ctsk 10505 |
. 2
class
Tarski |
2 | | vz |
. . . . . . . . 9
setvar 𝑧 |
3 | 2 | cv 1541 |
. . . . . . . 8
class 𝑧 |
4 | 3 | cpw 4539 |
. . . . . . 7
class 𝒫
𝑧 |
5 | | vy |
. . . . . . . 8
setvar 𝑦 |
6 | 5 | cv 1541 |
. . . . . . 7
class 𝑦 |
7 | 4, 6 | wss 3892 |
. . . . . 6
wff 𝒫
𝑧 ⊆ 𝑦 |
8 | | vw |
. . . . . . . . 9
setvar 𝑤 |
9 | 8 | cv 1541 |
. . . . . . . 8
class 𝑤 |
10 | 4, 9 | wss 3892 |
. . . . . . 7
wff 𝒫
𝑧 ⊆ 𝑤 |
11 | 10, 8, 6 | wrex 3067 |
. . . . . 6
wff
∃𝑤 ∈
𝑦 𝒫 𝑧 ⊆ 𝑤 |
12 | 7, 11 | wa 396 |
. . . . 5
wff (𝒫
𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) |
13 | 12, 2, 6 | wral 3066 |
. . . 4
wff
∀𝑧 ∈
𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) |
14 | | cen 8713 |
. . . . . . 7
class
≈ |
15 | 3, 6, 14 | wbr 5079 |
. . . . . 6
wff 𝑧 ≈ 𝑦 |
16 | 2, 5 | wel 2111 |
. . . . . 6
wff 𝑧 ∈ 𝑦 |
17 | 15, 16 | wo 844 |
. . . . 5
wff (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦) |
18 | 6 | cpw 4539 |
. . . . 5
class 𝒫
𝑦 |
19 | 17, 2, 18 | wral 3066 |
. . . 4
wff
∀𝑧 ∈
𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦) |
20 | 13, 19 | wa 396 |
. . 3
wff
(∀𝑧 ∈
𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) |
21 | 20, 5 | cab 2717 |
. 2
class {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))} |
22 | 1, 21 | wceq 1542 |
1
wff Tarski =
{𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))} |