Detailed syntax breakdown of Definition df-siga
Step | Hyp | Ref
| Expression |
1 | | csiga 32072 |
. 2
class
sigAlgebra |
2 | | vo |
. . 3
setvar 𝑜 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | vs |
. . . . . . 7
setvar 𝑠 |
5 | 4 | cv 1541 |
. . . . . 6
class 𝑠 |
6 | 2 | cv 1541 |
. . . . . . 7
class 𝑜 |
7 | 6 | cpw 4539 |
. . . . . 6
class 𝒫
𝑜 |
8 | 5, 7 | wss 3892 |
. . . . 5
wff 𝑠 ⊆ 𝒫 𝑜 |
9 | 2, 4 | wel 2111 |
. . . . . 6
wff 𝑜 ∈ 𝑠 |
10 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
11 | 10 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
12 | 6, 11 | cdif 3889 |
. . . . . . . 8
class (𝑜 ∖ 𝑥) |
13 | 12, 5 | wcel 2110 |
. . . . . . 7
wff (𝑜 ∖ 𝑥) ∈ 𝑠 |
14 | 13, 10, 5 | wral 3066 |
. . . . . 6
wff
∀𝑥 ∈
𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 |
15 | | com 7706 |
. . . . . . . . 9
class
ω |
16 | | cdom 8714 |
. . . . . . . . 9
class
≼ |
17 | 11, 15, 16 | wbr 5079 |
. . . . . . . 8
wff 𝑥 ≼
ω |
18 | 11 | cuni 4845 |
. . . . . . . . 9
class ∪ 𝑥 |
19 | 18, 5 | wcel 2110 |
. . . . . . . 8
wff ∪ 𝑥
∈ 𝑠 |
20 | 17, 19 | wi 4 |
. . . . . . 7
wff (𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠) |
21 | 5 | cpw 4539 |
. . . . . . 7
class 𝒫
𝑠 |
22 | 20, 10, 21 | wral 3066 |
. . . . . 6
wff
∀𝑥 ∈
𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠) |
23 | 9, 14, 22 | w3a 1086 |
. . . . 5
wff (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)) |
24 | 8, 23 | wa 396 |
. . . 4
wff (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))) |
25 | 24, 4 | cab 2717 |
. . 3
class {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} |
26 | 2, 3, 25 | cmpt 5162 |
. 2
class (𝑜 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))}) |
27 | 1, 26 | wceq 1542 |
1
wff sigAlgebra
= (𝑜 ∈ V ↦
{𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))}) |