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 e. Top -> ( Clsd ` J ) C_ ( sigaGen ` J ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 cldss 
 |-  ( x e. ( Clsd ` J ) -> x C_ U. J )
3 2 adantl 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> x C_ U. J )
4 dfss4 
 |-  ( x C_ U. J <-> ( U. J \ ( U. J \ x ) ) = x )
5 3 4 sylib 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( U. J \ ( U. J \ x ) ) = x )
6 1 topopn 
 |-  ( J e. Top -> U. J e. J )
7 1 difopn 
 |-  ( ( U. J e. J /\ x e. ( Clsd ` J ) ) -> ( U. J \ x ) e. J )
8 6 7 sylan 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( U. J \ x ) e. J )
9 id 
 |-  ( J e. Top -> J e. Top )
10 9 sgsiga 
 |-  ( J e. Top -> ( sigaGen ` J ) e. U. ran sigAlgebra )
11 10 adantr 
 |-  ( ( J e. Top /\ ( U. J \ x ) e. J ) -> ( sigaGen ` J ) e. U. ran sigAlgebra )
12 elex 
 |-  ( J e. Top -> J e. _V )
13 sigagensiga 
 |-  ( J e. _V -> ( sigaGen ` J ) e. ( sigAlgebra ` U. J ) )
14 baselsiga 
 |-  ( ( sigaGen ` J ) e. ( sigAlgebra ` U. J ) -> U. J e. ( sigaGen ` J ) )
15 12 13 14 3syl 
 |-  ( J e. Top -> U. J e. ( sigaGen ` J ) )
16 15 adantr 
 |-  ( ( J e. Top /\ ( U. J \ x ) e. J ) -> U. J e. ( sigaGen ` J ) )
17 elsigagen 
 |-  ( ( J e. Top /\ ( U. J \ x ) e. J ) -> ( U. J \ x ) e. ( sigaGen ` J ) )
18 difelsiga 
 |-  ( ( ( sigaGen ` J ) e. U. ran sigAlgebra /\ U. J e. ( sigaGen ` J ) /\ ( U. J \ x ) e. ( sigaGen ` J ) ) -> ( U. J \ ( U. J \ x ) ) e. ( sigaGen ` J ) )
19 11 16 17 18 syl3anc 
 |-  ( ( J e. Top /\ ( U. J \ x ) e. J ) -> ( U. J \ ( U. J \ x ) ) e. ( sigaGen ` J ) )
20 8 19 syldan 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> ( U. J \ ( U. J \ x ) ) e. ( sigaGen ` J ) )
21 5 20 eqeltrrd 
 |-  ( ( J e. Top /\ x e. ( Clsd ` J ) ) -> x e. ( sigaGen ` J ) )
22 21 ex 
 |-  ( J e. Top -> ( x e. ( Clsd ` J ) -> x e. ( sigaGen ` J ) ) )
23 22 ssrdv 
 |-  ( J e. Top -> ( Clsd ` J ) C_ ( sigaGen ` J ) )