Theorem dmsigagen

Description: A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017)

	Ref	Expression
Assertion	dmsigagen	⊢ dom sigaGen = V

Proof

Step	Hyp	Ref	Expression
1		vuniex	⊢ ∪ 𝑗 ∈ V
2		pwsiga	⊢ ( ∪ 𝑗 ∈ V → 𝒫 ∪ 𝑗 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) )
3	1 2	ax-mp	⊢ 𝒫 ∪ 𝑗 ∈ ( sigAlgebra ‘ ∪ 𝑗 )
4		pwuni	⊢ 𝑗 ⊆ 𝒫 ∪ 𝑗
5		sseq2	⊢ ( 𝑠 = 𝒫 ∪ 𝑗 → ( 𝑗 ⊆ 𝑠 ↔ 𝑗 ⊆ 𝒫 ∪ 𝑗 ) )
6	5	rspcev	⊢ ( ( 𝒫 ∪ 𝑗 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) ∧ 𝑗 ⊆ 𝒫 ∪ 𝑗 ) → ∃ 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) 𝑗 ⊆ 𝑠 )
7	3 4 6	mp2an	⊢ ∃ 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) 𝑗 ⊆ 𝑠
8		rabn0	⊢ ( { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) ∣ 𝑗 ⊆ 𝑠 } ≠ ∅ ↔ ∃ 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) 𝑗 ⊆ 𝑠 )
9	7 8	mpbir	⊢ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) ∣ 𝑗 ⊆ 𝑠 } ≠ ∅
10		intex	⊢ ( { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) ∣ 𝑗 ⊆ 𝑠 } ≠ ∅ ↔ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) ∣ 𝑗 ⊆ 𝑠 } ∈ V )
11	9 10	mpbi	⊢ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) ∣ 𝑗 ⊆ 𝑠 } ∈ V
12		df-sigagen	⊢ sigaGen = ( 𝑗 ∈ V ↦ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑗 ) ∣ 𝑗 ⊆ 𝑠 } )
13	11 12	dmmpti	⊢ dom sigaGen = V