Theorem sigagensiga

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

	Ref	Expression
Assertion	sigagensiga	⊢ ( 𝐴 ∈ 𝑉 → ( sigaGen ‘ 𝐴 ) ∈ ( sigAlgebra ‘ ∪ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sigagenval	⊢ ( 𝐴 ∈ 𝑉 → ( sigaGen ‘ 𝐴 ) = ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } )
2		fvex	⊢ ( sigaGen ‘ 𝐴 ) ∈ V
3	1 2	eqeltrrdi	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ∈ V )
4		intex	⊢ ( { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ≠ ∅ ↔ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ∈ V )
5	3 4	sylibr	⊢ ( 𝐴 ∈ 𝑉 → { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ≠ ∅ )
6		ssrab2	⊢ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ⊆ ( sigAlgebra ‘ ∪ 𝐴 )
7	6	a1i	⊢ ( 𝐴 ∈ 𝑉 → { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ⊆ ( sigAlgebra ‘ ∪ 𝐴 ) )
8		fvex	⊢ ( sigAlgebra ‘ ∪ 𝐴 ) ∈ V
9	8	elpw2	⊢ ( { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ∈ 𝒫 ( sigAlgebra ‘ ∪ 𝐴 ) ↔ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ⊆ ( sigAlgebra ‘ ∪ 𝐴 ) )
10	7 9	sylibr	⊢ ( 𝐴 ∈ 𝑉 → { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ∈ 𝒫 ( sigAlgebra ‘ ∪ 𝐴 ) )
11		insiga	⊢ ( ( { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ≠ ∅ ∧ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ∈ 𝒫 ( sigAlgebra ‘ ∪ 𝐴 ) ) → ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ∈ ( sigAlgebra ‘ ∪ 𝐴 ) )
12	5 10 11	syl2anc	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ∈ ( sigAlgebra ‘ ∪ 𝐴 ) )
13	1 12	eqeltrd	⊢ ( 𝐴 ∈ 𝑉 → ( sigaGen ‘ 𝐴 ) ∈ ( sigAlgebra ‘ ∪ 𝐴 ) )