Metamath Proof Explorer

Theorem bcth2

Description: Baire's Category Theorem, version 2: If countably many closed sets cover X , then one of them has an interior. (Contributed by Mario Carneiro, 10-Jan-2014)

Ref Expression
Hypothesis bcth.2 
|- J = ( MetOpen ` D )
Assertion bcth2 
|- ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> E. k e. NN ( ( int ` J ) ` ( M ` k ) ) =/= (/) )

Proof

Step Hyp Ref Expression
1 bcth.2 
 |-  J = ( MetOpen ` D )
2 simpll 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> D e. ( CMet ` X ) )
3 simprl 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> M : NN --> ( Clsd ` J ) )
4 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
5 4 ad2antrr 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> D e. ( Met ` X ) )
6 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
7 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
8 5 6 7 3syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> J e. ( TopOn ` X ) )
9 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
10 8 9 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> J e. Top )
11 simprr 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> U. ran M = X )
12 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
13 8 12 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> X e. J )
14 11 13 eqeltrd 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> U. ran M e. J )
15 isopn3i 
 |-  ( ( J e. Top /\ U. ran M e. J ) -> ( ( int ` J ) ` U. ran M ) = U. ran M )
16 10 14 15 syl2anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> ( ( int ` J ) ` U. ran M ) = U. ran M )
17 16 11 eqtrd 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> ( ( int ` J ) ` U. ran M ) = X )
18 simplr 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> X =/= (/) )
19 17 18 eqnetrd 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> ( ( int ` J ) ` U. ran M ) =/= (/) )
20 1 bcth 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) /\ ( ( int ` J ) ` U. ran M ) =/= (/) ) -> E. k e. NN ( ( int ` J ) ` ( M ` k ) ) =/= (/) )
21 2 3 19 20 syl3anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> E. k e. NN ( ( int ` J ) ` ( M ` k ) ) =/= (/) )