Metamath Proof Explorer

Theorem sigagensiga

Description: A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion sigagensiga ⊢ A ∈ V → 𝛔 ⁡ A ∈ sigAlgebra ⁡ ⋃ A

Proof

Step Hyp Ref Expression
1 sigagenval ⊢ A ∈ V → 𝛔 ⁡ A = ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s
2 fvex ⊢ 𝛔 ⁡ A ∈ V
3 1 2 eqeltrrdi ⊢ A ∈ V → ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ∈ V
4 intex ⊢ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ≠ ∅ ↔ ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ∈ V
5 3 4 sylibr ⊢ A ∈ V → s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ≠ ∅
6 ssrab2 ⊢ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ⊆ sigAlgebra ⁡ ⋃ A
7 6 a1i ⊢ A ∈ V → s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ⊆ sigAlgebra ⁡ ⋃ A
8 fvex ⊢ sigAlgebra ⁡ ⋃ A ∈ V
9 8 elpw2 ⊢ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ∈ 𝒫 sigAlgebra ⁡ ⋃ A ↔ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ⊆ sigAlgebra ⁡ ⋃ A
10 7 9 sylibr ⊢ A ∈ V → s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ∈ 𝒫 sigAlgebra ⁡ ⋃ A
11 insiga ⊢ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ≠ ∅ ∧ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ∈ 𝒫 sigAlgebra ⁡ ⋃ A → ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ∈ sigAlgebra ⁡ ⋃ A
12 5 10 11 syl2anc ⊢ A ∈ V → ⋂ s ∈ sigAlgebra ⁡ ⋃ A | A ⊆ s ∈ sigAlgebra ⁡ ⋃ A
13 1 12 eqeltrd ⊢ A ∈ V → 𝛔 ⁡ A ∈ sigAlgebra ⁡ ⋃ A