Metamath Proof Explorer

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 ⊢J∈Top→Clsd⁡J⊆𝛔⁡J

Proof

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