Step | Hyp | Ref
| Expression |
1 | | df-rab 2905 |
. . . 4
⊢ {𝑠 ∈ 𝒫 𝒫
𝑂 ∣ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))} = {𝑠 ∣ (𝑠 ∈ 𝒫 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} |
2 | | selpw 4115 |
. . . . . 6
⊢ (𝑠 ∈ 𝒫 𝒫
𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂) |
3 | 2 | anbi1i 727 |
. . . . 5
⊢ ((𝑠 ∈ 𝒫 𝒫
𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))) |
4 | 3 | abbii 2726 |
. . . 4
⊢ {𝑠 ∣ (𝑠 ∈ 𝒫 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} = {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} |
5 | 1, 4 | eqtri 2632 |
. . 3
⊢ {𝑠 ∈ 𝒫 𝒫
𝑂 ∣ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))} = {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} |
6 | | pwexg 4776 |
. . . 4
⊢ (𝑂 ∈ V → 𝒫 𝑂 ∈ V) |
7 | | pwexg 4776 |
. . . 4
⊢
(𝒫 𝑂 ∈
V → 𝒫 𝒫 𝑂 ∈ V) |
8 | | rabexg 4739 |
. . . 4
⊢
(𝒫 𝒫 𝑂 ∈ V → {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))} ∈
V) |
9 | 6, 7, 8 | 3syl 18 |
. . 3
⊢ (𝑂 ∈ V → {𝑠 ∈ 𝒫 𝒫
𝑂 ∣ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))} ∈
V) |
10 | 5, 9 | syl5eqelr 2693 |
. 2
⊢ (𝑂 ∈ V → {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} ∈
V) |
11 | | pweq 4111 |
. . . . . 6
⊢ (𝑜 = 𝑂 → 𝒫 𝑜 = 𝒫 𝑂) |
12 | 11 | sseq2d 3596 |
. . . . 5
⊢ (𝑜 = 𝑂 → (𝑠 ⊆ 𝒫 𝑜 ↔ 𝑠 ⊆ 𝒫 𝑂)) |
13 | | eleq1 2676 |
. . . . . 6
⊢ (𝑜 = 𝑂 → (𝑜 ∈ 𝑠 ↔ 𝑂 ∈ 𝑠)) |
14 | | difeq1 3683 |
. . . . . . . 8
⊢ (𝑜 = 𝑂 → (𝑜 ∖ 𝑥) = (𝑂 ∖ 𝑥)) |
15 | 14 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑜 = 𝑂 → ((𝑜 ∖ 𝑥) ∈ 𝑠 ↔ (𝑂 ∖ 𝑥) ∈ 𝑠)) |
16 | 15 | ralbidv 2969 |
. . . . . 6
⊢ (𝑜 = 𝑂 → (∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ↔ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠)) |
17 | 13, 16 | 3anbi12d 1392 |
. . . . 5
⊢ (𝑜 = 𝑂 → ((𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)) ↔ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))) |
18 | 12, 17 | anbi12d 743 |
. . . 4
⊢ (𝑜 = 𝑂 → ((𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))))) |
19 | 18 | abbidv 2728 |
. . 3
⊢ (𝑜 = 𝑂 → {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} = {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))}) |
20 | | df-siga 29498 |
. . 3
⊢
sigAlgebra = (𝑜
∈ V ↦ {𝑠 ∣
(𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))}) |
21 | 19, 20 | fvmptg 6189 |
. 2
⊢ ((𝑂 ∈ V ∧ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} ∈ V)
→ (sigAlgebra‘𝑂)
= {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))}) |
22 | 10, 21 | mpdan 699 |
1
⊢ (𝑂 ∈ V →
(sigAlgebra‘𝑂) =
{𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))}) |