Step | Hyp | Ref
| Expression |
1 | | df-siga 29498 |
. . 3
⊢
sigAlgebra = (𝑜
∈ V ↦ {𝑠 ∣
(𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))}) |
2 | | df-rab 2905 |
. . . . 5
⊢ {𝑠 ∈ 𝒫 𝒫
𝑜 ∣ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))} = {𝑠 ∣ (𝑠 ∈ 𝒫 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} |
3 | | vex 3176 |
. . . . . . . 8
⊢ 𝑠 ∈ V |
4 | | elpwg 4116 |
. . . . . . . 8
⊢ (𝑠 ∈ V → (𝑠 ∈ 𝒫 𝒫
𝑜 ↔ 𝑠 ⊆ 𝒫 𝑜)) |
5 | 3, 4 | ax-mp 5 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝒫
𝑜 ↔ 𝑠 ⊆ 𝒫 𝑜) |
6 | 5 | anbi1i 727 |
. . . . . 6
⊢ ((𝑠 ∈ 𝒫 𝒫
𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))) ↔ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))) |
7 | 6 | abbii 2726 |
. . . . 5
⊢ {𝑠 ∣ (𝑠 ∈ 𝒫 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} = {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} |
8 | 2, 7 | eqtr2i 2633 |
. . . 4
⊢ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} = {𝑠 ∈ 𝒫 𝒫
𝑜 ∣ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))} |
9 | | grothpwex 9528 |
. . . . . 6
⊢ 𝒫
𝑜 ∈ V |
10 | 9 | pwex 4774 |
. . . . 5
⊢ 𝒫
𝒫 𝑜 ∈
V |
11 | 10 | rabex 4740 |
. . . 4
⊢ {𝑠 ∈ 𝒫 𝒫
𝑜 ∣ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))} ∈
V |
12 | 8, 11 | eqeltri 2684 |
. . 3
⊢ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} ∈
V |
13 | | sseq1 3589 |
. . . 4
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝒫 𝑜 ↔ 𝑆 ⊆ 𝒫 𝑜)) |
14 | | eleq2 2677 |
. . . . 5
⊢ (𝑠 = 𝑆 → (𝑜 ∈ 𝑠 ↔ 𝑜 ∈ 𝑆)) |
15 | | eleq2 2677 |
. . . . . 6
⊢ (𝑠 = 𝑆 → ((𝑜 ∖ 𝑥) ∈ 𝑠 ↔ (𝑜 ∖ 𝑥) ∈ 𝑆)) |
16 | 15 | raleqbi1dv 3123 |
. . . . 5
⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ↔ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆)) |
17 | | pweq 4111 |
. . . . . 6
⊢ (𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆) |
18 | | biidd 251 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (𝑥 ≼ ω ↔ 𝑥 ≼ ω)) |
19 | | eleq2 2677 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (∪ 𝑥 ∈ 𝑠 ↔ ∪ 𝑥 ∈ 𝑆)) |
20 | 18, 19 | imbi12d 333 |
. . . . . 6
⊢ (𝑠 = 𝑆 → ((𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠) ↔ (𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) |
21 | 17, 20 | raleqbidv 3129 |
. . . . 5
⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠) ↔
∀𝑥 ∈ 𝒫
𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) |
22 | 14, 16, 21 | 3anbi123d 1391 |
. . . 4
⊢ (𝑠 = 𝑆 → ((𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)) ↔ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) |
23 | 13, 22 | anbi12d 743 |
. . 3
⊢ (𝑠 = 𝑆 → ((𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))) ↔ (𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) |
24 | 1, 12, 23 | abfmpunirn 28832 |
. 2
⊢ (𝑆 ∈ ∪ ran sigAlgebra ↔ (𝑆 ∈ V ∧ ∃𝑜 ∈ V (𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) |
25 | | rexv 3193 |
. . 3
⊢
(∃𝑜 ∈ V
(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) ↔
∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) |
26 | 25 | anbi2i 726 |
. 2
⊢ ((𝑆 ∈ V ∧ ∃𝑜 ∈ V (𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) ↔ (𝑆 ∈ V ∧ ∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) |
27 | 24, 26 | bitri 263 |
1
⊢ (𝑆 ∈ ∪ ran sigAlgebra ↔ (𝑆 ∈ V ∧ ∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) |