Detailed syntax breakdown of Definition df-sigagen
Step | Hyp | Ref
| Expression |
1 | | csigagen 31818 |
. 2
class
sigaGen |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cvv 3408 |
. . 3
class
V |
4 | 2 | cv 1542 |
. . . . . 6
class 𝑥 |
5 | | vs |
. . . . . . 7
setvar 𝑠 |
6 | 5 | cv 1542 |
. . . . . 6
class 𝑠 |
7 | 4, 6 | wss 3866 |
. . . . 5
wff 𝑥 ⊆ 𝑠 |
8 | 4 | cuni 4819 |
. . . . . 6
class ∪ 𝑥 |
9 | | csiga 31788 |
. . . . . 6
class
sigAlgebra |
10 | 8, 9 | cfv 6380 |
. . . . 5
class
(sigAlgebra‘∪ 𝑥) |
11 | 7, 5, 10 | crab 3065 |
. . . 4
class {𝑠 ∈ (sigAlgebra‘∪ 𝑥)
∣ 𝑥 ⊆ 𝑠} |
12 | 11 | cint 4859 |
. . 3
class ∩ {𝑠
∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠} |
13 | 2, 3, 12 | cmpt 5135 |
. 2
class (𝑥 ∈ V ↦ ∩ {𝑠
∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠}) |
14 | 1, 13 | wceq 1543 |
1
wff sigaGen =
(𝑥 ∈ V ↦ ∩ {𝑠
∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠}) |