| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fvssunirn 6938 | . . . 4
⊢
(sigAlgebra‘𝑂)
⊆ ∪ ran sigAlgebra | 
| 2 | 1 | sseli 3978 | . . 3
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran
sigAlgebra) | 
| 3 |  | elex 3500 | . . . 4
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ V) | 
| 4 |  | issiga 34114 | . . . . 5
⊢ (𝑆 ∈ V → (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) | 
| 5 |  | elpwuni 5104 | . . . . . . . 8
⊢ (𝑂 ∈ 𝑆 → (𝑆 ⊆ 𝒫 𝑂 ↔ ∪ 𝑆 = 𝑂)) | 
| 6 | 5 | biimpa 476 | . . . . . . 7
⊢ ((𝑂 ∈ 𝑆 ∧ 𝑆 ⊆ 𝒫 𝑂) → ∪ 𝑆 = 𝑂) | 
| 7 |  | ancom 460 | . . . . . . 7
⊢ ((𝑆 ⊆ 𝒫 𝑂 ∧ 𝑂 ∈ 𝑆) ↔ (𝑂 ∈ 𝑆 ∧ 𝑆 ⊆ 𝒫 𝑂)) | 
| 8 |  | eqcom 2743 | . . . . . . 7
⊢ (𝑂 = ∪
𝑆 ↔ ∪ 𝑆 =
𝑂) | 
| 9 | 6, 7, 8 | 3imtr4i 292 | . . . . . 6
⊢ ((𝑆 ⊆ 𝒫 𝑂 ∧ 𝑂 ∈ 𝑆) → 𝑂 = ∪ 𝑆) | 
| 10 | 9 | 3ad2antr1 1188 | . . . . 5
⊢ ((𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → 𝑂 = ∪
𝑆) | 
| 11 | 4, 10 | biimtrdi 253 | . . . 4
⊢ (𝑆 ∈ V → (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑂 = ∪ 𝑆)) | 
| 12 | 3, 11 | mpcom 38 | . . 3
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑂 = ∪ 𝑆) | 
| 13 | 2, 12 | jca 511 | . 2
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → (𝑆 ∈ ∪ ran
sigAlgebra ∧ 𝑂 = ∪ 𝑆)) | 
| 14 |  | elex 3500 | . . . . 5
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ V) | 
| 15 |  | isrnsiga 34115 | . . . . . . . 8
⊢ (𝑆 ∈ ∪ ran sigAlgebra ↔ (𝑆 ∈ V ∧ ∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) | 
| 16 | 15 | simprbi 496 | . . . . . . 7
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) | 
| 17 |  | elpwuni 5104 | . . . . . . . . . . . . 13
⊢ (𝑜 ∈ 𝑆 → (𝑆 ⊆ 𝒫 𝑜 ↔ ∪ 𝑆 = 𝑜)) | 
| 18 | 17 | biimpa 476 | . . . . . . . . . . . 12
⊢ ((𝑜 ∈ 𝑆 ∧ 𝑆 ⊆ 𝒫 𝑜) → ∪ 𝑆 = 𝑜) | 
| 19 |  | ancom 460 | . . . . . . . . . . . 12
⊢ ((𝑆 ⊆ 𝒫 𝑜 ∧ 𝑜 ∈ 𝑆) ↔ (𝑜 ∈ 𝑆 ∧ 𝑆 ⊆ 𝒫 𝑜)) | 
| 20 |  | eqcom 2743 | . . . . . . . . . . . 12
⊢ (𝑜 = ∪
𝑆 ↔ ∪ 𝑆 =
𝑜) | 
| 21 | 18, 19, 20 | 3imtr4i 292 | . . . . . . . . . . 11
⊢ ((𝑆 ⊆ 𝒫 𝑜 ∧ 𝑜 ∈ 𝑆) → 𝑜 = ∪ 𝑆) | 
| 22 | 21 | 3ad2antr1 1188 | . . . . . . . . . 10
⊢ ((𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → 𝑜 = ∪
𝑆) | 
| 23 |  | pweq 4613 | . . . . . . . . . . . 12
⊢ (𝑜 = ∪
𝑆 → 𝒫 𝑜 = 𝒫 ∪ 𝑆) | 
| 24 | 23 | sseq2d 4015 | . . . . . . . . . . 11
⊢ (𝑜 = ∪
𝑆 → (𝑆 ⊆ 𝒫 𝑜 ↔ 𝑆 ⊆ 𝒫 ∪ 𝑆)) | 
| 25 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑜 = ∪
𝑆 → (𝑜 ∈ 𝑆 ↔ ∪ 𝑆 ∈ 𝑆)) | 
| 26 |  | difeq1 4118 | . . . . . . . . . . . . . 14
⊢ (𝑜 = ∪
𝑆 → (𝑜 ∖ 𝑥) = (∪ 𝑆 ∖ 𝑥)) | 
| 27 | 26 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑜 = ∪
𝑆 → ((𝑜 ∖ 𝑥) ∈ 𝑆 ↔ (∪ 𝑆 ∖ 𝑥) ∈ 𝑆)) | 
| 28 | 27 | ralbidv 3177 | . . . . . . . . . . . 12
⊢ (𝑜 = ∪
𝑆 → (∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ↔ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆)) | 
| 29 | 25, 28 | 3anbi12d 1438 | . . . . . . . . . . 11
⊢ (𝑜 = ∪
𝑆 → ((𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) ↔ (∪ 𝑆
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 (∪
𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) | 
| 30 | 24, 29 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑜 = ∪
𝑆 → ((𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) ↔ (𝑆 ⊆ 𝒫 ∪ 𝑆
∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) | 
| 31 | 22, 30 | syl 17 | . . . . . . . . 9
⊢ ((𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → ((𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) ↔ (𝑆 ⊆ 𝒫 ∪ 𝑆
∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) | 
| 32 | 31 | ibi 267 | . . . . . . . 8
⊢ ((𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → (𝑆 ⊆ 𝒫 ∪ 𝑆
∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) | 
| 33 | 32 | exlimiv 1929 | . . . . . . 7
⊢
(∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → (𝑆 ⊆ 𝒫 ∪ 𝑆
∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) | 
| 34 | 16, 33 | syl 17 | . . . . . 6
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆
∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) | 
| 35 | 34 | simprd 495 | . . . . 5
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (∪
𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) | 
| 36 | 14, 35 | jca 511 | . . . 4
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ∈ V ∧ (∪ 𝑆
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 (∪
𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) | 
| 37 |  | eleq1 2828 | . . . . . . . 8
⊢ (𝑂 = ∪
𝑆 → (𝑂 ∈ 𝑆 ↔ ∪ 𝑆 ∈ 𝑆)) | 
| 38 |  | difeq1 4118 | . . . . . . . . . 10
⊢ (𝑂 = ∪
𝑆 → (𝑂 ∖ 𝑥) = (∪ 𝑆 ∖ 𝑥)) | 
| 39 | 38 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑂 = ∪
𝑆 → ((𝑂 ∖ 𝑥) ∈ 𝑆 ↔ (∪ 𝑆 ∖ 𝑥) ∈ 𝑆)) | 
| 40 | 39 | ralbidv 3177 | . . . . . . . 8
⊢ (𝑂 = ∪
𝑆 → (∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ↔ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆)) | 
| 41 | 37, 40 | 3anbi12d 1438 | . . . . . . 7
⊢ (𝑂 = ∪
𝑆 → ((𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) ↔ (∪ 𝑆
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 (∪
𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) | 
| 42 | 41 | biimprd 248 | . . . . . 6
⊢ (𝑂 = ∪
𝑆 → ((∪ 𝑆
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 (∪
𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) → (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) | 
| 43 |  | pwuni 4944 | . . . . . . 7
⊢ 𝑆 ⊆ 𝒫 ∪ 𝑆 | 
| 44 |  | pweq 4613 | . . . . . . 7
⊢ (𝑂 = ∪
𝑆 → 𝒫 𝑂 = 𝒫 ∪ 𝑆) | 
| 45 | 43, 44 | sseqtrrid 4026 | . . . . . 6
⊢ (𝑂 = ∪
𝑆 → 𝑆 ⊆ 𝒫 𝑂) | 
| 46 | 42, 45 | jctild 525 | . . . . 5
⊢ (𝑂 = ∪
𝑆 → ((∪ 𝑆
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 (∪
𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)) → (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))))) | 
| 47 | 46 | anim2d 612 | . . . 4
⊢ (𝑂 = ∪
𝑆 → ((𝑆 ∈ V ∧ (∪ 𝑆
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 (∪
𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆))) → (𝑆 ∈ V ∧ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))))) | 
| 48 | 4 | biimpar 477 | . . . 4
⊢ ((𝑆 ∈ V ∧ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥
∈ 𝑆)))) → 𝑆 ∈ (sigAlgebra‘𝑂)) | 
| 49 | 36, 47, 48 | syl56 36 | . . 3
⊢ (𝑂 = ∪
𝑆 → (𝑆 ∈ ∪ ran
sigAlgebra → 𝑆 ∈
(sigAlgebra‘𝑂))) | 
| 50 | 49 | impcom 407 | . 2
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑂 = ∪ 𝑆) → 𝑆 ∈ (sigAlgebra‘𝑂)) | 
| 51 | 13, 50 | impbii 209 | 1
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ∈ ∪ ran
sigAlgebra ∧ 𝑂 = ∪ 𝑆)) |