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