| Step | Hyp | Ref
| Expression |
| 1 | | elfvex 6944 |
. . . 4
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V) |
| 2 | | elex 3501 |
. . . 4
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ V) |
| 3 | 1, 2 | jca 511 |
. . 3
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → (𝑂 ∈ V ∧ 𝑆 ∈ V)) |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝑆 ∈ V → (𝑆 ∈ (sigAlgebra‘𝑂) → (𝑂 ∈ V ∧ 𝑆 ∈ V))) |
| 5 | | simpr1 1195 |
. . . . 5
⊢ ((𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → 𝑂 ∈ 𝑆) |
| 6 | | elex 3501 |
. . . . 5
⊢ (𝑂 ∈ 𝑆 → 𝑂 ∈ V) |
| 7 | 5, 6 | syl 17 |
. . . 4
⊢ ((𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → 𝑂 ∈ V) |
| 8 | 7 | a1i 11 |
. . 3
⊢ (𝑆 ∈ V → ((𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → 𝑂 ∈ V)) |
| 9 | 8 | anc2ri 556 |
. 2
⊢ (𝑆 ∈ V → ((𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → (𝑂 ∈ V ∧ 𝑆 ∈ V))) |
| 10 | | df-siga 34110 |
. . . 4
⊢
sigAlgebra = (𝑜
∈ V ↦ {𝑠 ∣
(𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))}) |
| 11 | | sigaex 34111 |
. . . 4
⊢ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)))} ∈
V |
| 12 | | pweq 4614 |
. . . . . . 7
⊢ (𝑜 = 𝑂 → 𝒫 𝑜 = 𝒫 𝑂) |
| 13 | 12 | sseq2d 4016 |
. . . . . 6
⊢ (𝑜 = 𝑂 → (𝑠 ⊆ 𝒫 𝑜 ↔ 𝑠 ⊆ 𝒫 𝑂)) |
| 14 | | sseq1 4009 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝒫 𝑂 ↔ 𝑆 ⊆ 𝒫 𝑂)) |
| 15 | 13, 14 | sylan9bb 509 |
. . . . 5
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → (𝑠 ⊆ 𝒫 𝑜 ↔ 𝑆 ⊆ 𝒫 𝑂)) |
| 16 | | eleq12 2831 |
. . . . . 6
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → (𝑜 ∈ 𝑠 ↔ 𝑂 ∈ 𝑆)) |
| 17 | | simpr 484 |
. . . . . . 7
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) |
| 18 | | difeq1 4119 |
. . . . . . . . . 10
⊢ (𝑜 = 𝑂 → (𝑜 ∖ 𝑥) = (𝑂 ∖ 𝑥)) |
| 19 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → (𝑜 ∖ 𝑥) = (𝑂 ∖ 𝑥)) |
| 20 | 19 | eleq1d 2826 |
. . . . . . . 8
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → ((𝑜 ∖ 𝑥) ∈ 𝑠 ↔ (𝑂 ∖ 𝑥) ∈ 𝑠)) |
| 21 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑠 = 𝑆 → ((𝑂 ∖ 𝑥) ∈ 𝑠 ↔ (𝑂 ∖ 𝑥) ∈ 𝑆)) |
| 22 | 21 | adantl 481 |
. . . . . . . 8
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → ((𝑂 ∖ 𝑥) ∈ 𝑠 ↔ (𝑂 ∖ 𝑥) ∈ 𝑆)) |
| 23 | 20, 22 | bitrd 279 |
. . . . . . 7
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → ((𝑜 ∖ 𝑥) ∈ 𝑠 ↔ (𝑂 ∖ 𝑥) ∈ 𝑆)) |
| 24 | 17, 23 | raleqbidv 3346 |
. . . . . 6
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → (∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ↔ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆)) |
| 25 | | pweq 4614 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆) |
| 26 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑠 = 𝑆 → (∪ 𝑥 ∈ 𝑠 ↔ ∪ 𝑥 ∈ 𝑆)) |
| 27 | 26 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → ((𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠) ↔ (𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) |
| 28 | 25, 27 | raleqbidv 3346 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠) ↔
∀𝑥 ∈ 𝒫
𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) |
| 29 | 28 | adantl 481 |
. . . . . 6
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → (∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠) ↔
∀𝑥 ∈ 𝒫
𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) |
| 30 | 16, 24, 29 | 3anbi123d 1438 |
. . . . 5
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → ((𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠)) ↔ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) |
| 31 | 15, 30 | anbi12d 632 |
. . . 4
⊢ ((𝑜 = 𝑂 ∧ 𝑠 = 𝑆) → ((𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑠))) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) |
| 32 | 10, 11, 31 | abfmpel 32665 |
. . 3
⊢ ((𝑂 ∈ V ∧ 𝑆 ∈ V) → (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) |
| 33 | 32 | a1i 11 |
. 2
⊢ (𝑆 ∈ V → ((𝑂 ∈ V ∧ 𝑆 ∈ V) → (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))))) |
| 34 | 4, 9, 33 | pm5.21ndd 379 |
1
⊢ (𝑆 ∈ V → (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) |