Detailed syntax breakdown of Definition df-fbas
Step | Hyp | Ref
| Expression |
1 | | cfbas 12623 |
. 2
class
fBas |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 2726 |
. . 3
class
V |
4 | | vx |
. . . . . . 7
setvar 𝑥 |
5 | 4 | cv 1342 |
. . . . . 6
class 𝑥 |
6 | | c0 3409 |
. . . . . 6
class
∅ |
7 | 5, 6 | wne 2336 |
. . . . 5
wff 𝑥 ≠ ∅ |
8 | 6, 5 | wnel 2431 |
. . . . 5
wff ∅
∉ 𝑥 |
9 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
10 | 9 | cv 1342 |
. . . . . . . . . . 11
class 𝑦 |
11 | | vz |
. . . . . . . . . . . 12
setvar 𝑧 |
12 | 11 | cv 1342 |
. . . . . . . . . . 11
class 𝑧 |
13 | 10, 12 | cin 3115 |
. . . . . . . . . 10
class (𝑦 ∩ 𝑧) |
14 | 13 | cpw 3559 |
. . . . . . . . 9
class 𝒫
(𝑦 ∩ 𝑧) |
15 | 5, 14 | cin 3115 |
. . . . . . . 8
class (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) |
16 | 15, 6 | wne 2336 |
. . . . . . 7
wff (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅ |
17 | 16, 11, 5 | wral 2444 |
. . . . . 6
wff
∀𝑧 ∈
𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅ |
18 | 17, 9, 5 | wral 2444 |
. . . . 5
wff
∀𝑦 ∈
𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅ |
19 | 7, 8, 18 | w3a 968 |
. . . 4
wff (𝑥 ≠ ∅ ∧ ∅
∉ 𝑥 ∧
∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅) |
20 | 2 | cv 1342 |
. . . . . 6
class 𝑤 |
21 | 20 | cpw 3559 |
. . . . 5
class 𝒫
𝑤 |
22 | 21 | cpw 3559 |
. . . 4
class 𝒫
𝒫 𝑤 |
23 | 19, 4, 22 | crab 2448 |
. . 3
class {𝑥 ∈ 𝒫 𝒫
𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅
∉ 𝑥 ∧
∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)} |
24 | 2, 3, 23 | cmpt 4043 |
. 2
class (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫
𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅
∉ 𝑥 ∧
∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)}) |
25 | 1, 24 | wceq 1343 |
1
wff fBas =
(𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫
𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅
∉ 𝑥 ∧
∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)}) |