Theorem cldssbrsiga

Description: A Borel Algebra contains all closed sets of its base topology. (Contributed by Thierry Arnoux, 27-Mar-2017)

	Ref	Expression
Assertion	cldssbrsiga	⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	cldss	⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ ∪ 𝐽 )
3	2	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ⊆ ∪ 𝐽 )
4		dfss4	⊢ ( 𝑥 ⊆ ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) = 𝑥 )
5	3 4	sylib	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) = 𝑥 )
6	1	topopn	⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 )
7	1	difopn	⊢ ( ( ∪ 𝐽 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 )
8	6 7	sylan	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 )
9		id	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ Top )
10	9	sgsiga	⊢ ( 𝐽 ∈ Top → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra )
11	10	adantr	⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra )
12		elex	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ V )
13		sigagensiga	⊢ ( 𝐽 ∈ V → ( sigaGen ‘ 𝐽 ) ∈ ( sigAlgebra ‘ ∪ 𝐽 ) )
14		baselsiga	⊢ ( ( sigaGen ‘ 𝐽 ) ∈ ( sigAlgebra ‘ ∪ 𝐽 ) → ∪ 𝐽 ∈ ( sigaGen ‘ 𝐽 ) )
15	12 13 14	3syl	⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ ( sigaGen ‘ 𝐽 ) )
16	15	adantr	⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) → ∪ 𝐽 ∈ ( sigaGen ‘ 𝐽 ) )
17		elsigagen	⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( sigaGen ‘ 𝐽 ) )
18		difelsiga	⊢ ( ( ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra ∧ ∪ 𝐽 ∈ ( sigaGen ‘ 𝐽 ) ∧ ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( sigaGen ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ∈ ( sigaGen ‘ 𝐽 ) )
19	11 16 17 18	syl3anc	⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ∈ ( sigaGen ‘ 𝐽 ) )
20	8 19	syldan	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ∈ ( sigaGen ‘ 𝐽 ) )
21	5 20	eqeltrrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ ( sigaGen ‘ 𝐽 ) )
22	21	ex	⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ∈ ( sigaGen ‘ 𝐽 ) ) )
23	22	ssrdv	⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) )