Detailed syntax breakdown of Definition df-fg
Step | Hyp | Ref
| Expression |
1 | | cfg 20352 |
. 2
class
filGen |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | vx |
. . 3
setvar 𝑥 |
4 | | cvv 3408 |
. . 3
class
V |
5 | 2 | cv 1542 |
. . . 4
class 𝑤 |
6 | | cfbas 20351 |
. . . 4
class
fBas |
7 | 5, 6 | cfv 6380 |
. . 3
class
(fBas‘𝑤) |
8 | 3 | cv 1542 |
. . . . . 6
class 𝑥 |
9 | | vy |
. . . . . . . 8
setvar 𝑦 |
10 | 9 | cv 1542 |
. . . . . . 7
class 𝑦 |
11 | 10 | cpw 4513 |
. . . . . 6
class 𝒫
𝑦 |
12 | 8, 11 | cin 3865 |
. . . . 5
class (𝑥 ∩ 𝒫 𝑦) |
13 | | c0 4237 |
. . . . 5
class
∅ |
14 | 12, 13 | wne 2940 |
. . . 4
wff (𝑥 ∩ 𝒫 𝑦) ≠ ∅ |
15 | 5 | cpw 4513 |
. . . 4
class 𝒫
𝑤 |
16 | 14, 9, 15 | crab 3065 |
. . 3
class {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅} |
17 | 2, 3, 4, 7, 16 | cmpo 7215 |
. 2
class (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅}) |
18 | 1, 17 | wceq 1543 |
1
wff filGen =
(𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅}) |