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 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
Assertion bcth2 ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ βˆƒ π‘˜ ∈ β„• ( ( int β€˜ 𝐽 ) β€˜ ( 𝑀 β€˜ π‘˜ ) ) β‰  βˆ… )

Proof

Step Hyp Ref Expression
1 bcth.2 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
2 simpll ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ 𝐷 ∈ ( CMet β€˜ 𝑋 ) )
3 simprl ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) )
4 cmetmet ⊒ ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
5 4 ad2antrr ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
6 metxmet ⊒ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
7 1 mopntopon ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
8 5 6 7 3syl ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
9 topontop ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ 𝐽 ∈ Top )
10 8 9 syl ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ 𝐽 ∈ Top )
11 simprr ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ βˆͺ ran 𝑀 = 𝑋 )
12 toponmax ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ 𝑋 ∈ 𝐽 )
13 8 12 syl ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ 𝑋 ∈ 𝐽 )
14 11 13 eqeltrd ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ βˆͺ ran 𝑀 ∈ 𝐽 )
15 isopn3i ⊒ ( ( 𝐽 ∈ Top ∧ βˆͺ ran 𝑀 ∈ 𝐽 ) β†’ ( ( int β€˜ 𝐽 ) β€˜ βˆͺ ran 𝑀 ) = βˆͺ ran 𝑀 )
16 10 14 15 syl2anc ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ ( ( int β€˜ 𝐽 ) β€˜ βˆͺ ran 𝑀 ) = βˆͺ ran 𝑀 )
17 16 11 eqtrd ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ ( ( int β€˜ 𝐽 ) β€˜ βˆͺ ran 𝑀 ) = 𝑋 )
18 simplr ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ 𝑋 β‰  βˆ… )
19 17 18 eqnetrd ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ ( ( int β€˜ 𝐽 ) β€˜ βˆͺ ran 𝑀 ) β‰  βˆ… )
20 1 bcth ⊒ ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ ( ( int β€˜ 𝐽 ) β€˜ βˆͺ ran 𝑀 ) β‰  βˆ… ) β†’ βˆƒ π‘˜ ∈ β„• ( ( int β€˜ 𝐽 ) β€˜ ( 𝑀 β€˜ π‘˜ ) ) β‰  βˆ… )
21 2 3 19 20 syl3anc ⊒ ( ( ( 𝐷 ∈ ( CMet β€˜ 𝑋 ) ∧ 𝑋 β‰  βˆ… ) ∧ ( 𝑀 : β„• ⟢ ( Clsd β€˜ 𝐽 ) ∧ βˆͺ ran 𝑀 = 𝑋 ) ) β†’ βˆƒ π‘˜ ∈ β„• ( ( int β€˜ 𝐽 ) β€˜ ( 𝑀 β€˜ π‘˜ ) ) β‰  βˆ… )