Theorem brsiga

Description: The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

	Ref	Expression
Assertion	brsiga	⊢ 𝔅ℝ ∈ ( sigaGen “ Top )

Proof

Step	Hyp	Ref	Expression
1		df-brsiga	⊢ 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) )
2		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
3		df-sigagen	⊢ sigaGen = ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 } )
4	3	funmpt2	⊢ Fun sigaGen
5		fvex	⊢ ( topGen ‘ ran (,) ) ∈ V
6		sigagensiga	⊢ ( ( topGen ‘ ran (,) ) ∈ V → ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ( sigAlgebra ‘ ∪ ( topGen ‘ ran (,) ) ) )
7		elrnsiga	⊢ ( ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ( sigAlgebra ‘ ∪ ( topGen ‘ ran (,) ) ) → ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ∪ ran sigAlgebra )
8	5 6 7	mp2b	⊢ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ∪ ran sigAlgebra
9		0elsiga	⊢ ( ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ∪ ran sigAlgebra → ∅ ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
10		elfvdm	⊢ ( ∅ ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) → ( topGen ‘ ran (,) ) ∈ dom sigaGen )
11	8 9 10	mp2b	⊢ ( topGen ‘ ran (,) ) ∈ dom sigaGen
12		funfvima	⊢ ( ( Fun sigaGen ∧ ( topGen ‘ ran (,) ) ∈ dom sigaGen ) → ( ( topGen ‘ ran (,) ) ∈ Top → ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ( sigaGen “ Top ) ) )
13	4 11 12	mp2an	⊢ ( ( topGen ‘ ran (,) ) ∈ Top → ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ( sigaGen “ Top ) )
14	2 13	ax-mp	⊢ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ( sigaGen “ Top )
15	1 14	eqeltri	⊢ 𝔅ℝ ∈ ( sigaGen “ Top )