Metamath Proof Explorer

Theorem sigagenval

Description: Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion sigagenval ⊢ A ∈ V → 𝛔 ⁡ A = ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s

Proof

Step Hyp Ref Expression
1 df-sigagen ⊢ 𝛔 = x ∈ V ⟼ ⋂ s ∈ sigAlgebra ⁡ ⋃ x | x ⊆ s
2 1 a1i ⊢ A ∈ V → 𝛔 = x ∈ V ⟼ ⋂ s ∈ sigAlgebra ⁡ ⋃ x | x ⊆ s
3 unieq ⊢ x = A → ⋃ x = ⋃ A
4 3 fveq2d ⊢ x = A → sigAlgebra ⁡ ⋃ x = sigAlgebra ⁡ ⋃ A
5 sseq1 ⊢ x = A → x ⊆ s ↔ A ⊆ s
6 4 5 rabeqbidv ⊢ x = A → s ∈ sigAlgebra ⁡ ⋃ x | x ⊆ s = s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s
7 6 inteqd ⊢ x = A → ⋂ s ∈ sigAlgebra ⁡ ⋃ x | x ⊆ s = ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s
8 7 adantl ⊢ A ∈ V ∧ x = A → ⋂ s ∈ sigAlgebra ⁡ ⋃ x | x ⊆ s = ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s
9 elex ⊢ A ∈ V → A ∈ V
10 uniexg ⊢ A ∈ V → ⋃ A ∈ V
11 pwsiga ⊢ ⋃ A ∈ V → 𝒫 ⋃ A ∈ sigAlgebra ⁡ ⋃ A
12 10 11 syl ⊢ A ∈ V → 𝒫 ⋃ A ∈ sigAlgebra ⁡ ⋃ A
13 pwuni ⊢ A ⊆ 𝒫 ⋃ A
14 12 13 jctir ⊢ A ∈ V → 𝒫 ⋃ A ∈ sigAlgebra ⁡ ⋃ A ∧ A ⊆ 𝒫 ⋃ A
15 sseq2 ⊢ s = 𝒫 ⋃ A → A ⊆ s ↔ A ⊆ 𝒫 ⋃ A
16 15 elrab ⊢ 𝒫 ⋃ A ∈ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ↔ 𝒫 ⋃ A ∈ sigAlgebra ⁡ ⋃ A ∧ A ⊆ 𝒫 ⋃ A
17 14 16 sylibr ⊢ A ∈ V → 𝒫 ⋃ A ∈ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s
18 17 ne0d ⊢ A ∈ V → s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ≠ ∅
19 intex ⊢ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ≠ ∅ ↔ ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ∈ V
20 18 19 sylib ⊢ A ∈ V → ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ∈ V
21 2 8 9 20 fvmptd ⊢ A ∈ V → 𝛔 ⁡ A = ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s