This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bcth3

Description: Baire's Category Theorem, version 3: The intersection of countably many dense open sets is dense. (Contributed by Mario Carneiro, 10-Jan-2014)

Ref Expression
Hypothesis bcth.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion bcth3 ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( ( cls ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑀 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 bcth.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 2 3 syl ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
5 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
6 5 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → 𝐽 ∈ Top )
7 ffvelcdm ⊢ ( ( 𝑀 : ℕ ⟶ 𝐽 ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ 𝑘 ) ∈ 𝐽 )
8 elssuni ⊢ ( ( 𝑀 ‘ 𝑘 ) ∈ 𝐽 → ( 𝑀 ‘ 𝑘 ) ⊆ ∪ 𝐽 )
9 7 8 syl ⊢ ( ( 𝑀 : ℕ ⟶ 𝐽 ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ 𝑘 ) ⊆ ∪ 𝐽 )
10 9 adantll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ 𝑘 ) ⊆ ∪ 𝐽 )
11 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
12 11 clsval2 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑀 ‘ 𝑘 ) ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) )
13 6 10 12 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) )
14 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
15 14 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → 𝑋 = ∪ 𝐽 )
16 13 15 eqeq12d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = 𝑋 ↔ ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) = ∪ 𝐽 ) )
17 difeq2 ⊢ ( ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) = ( ∪ 𝐽 ∖ ∪ 𝐽 ) )
18 difid ⊢ ( ∪ 𝐽 ∖ ∪ 𝐽 ) = ∅
19 17 18 eqtrdi ⊢ ( ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) = ∅ )
20 difss ⊢ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ⊆ ∪ 𝐽
21 11 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ∈ 𝐽 )
22 6 20 21 sylancl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ∈ 𝐽 )
23 elssuni ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ∈ 𝐽 → ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ⊆ ∪ 𝐽 )
24 22 23 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ⊆ ∪ 𝐽 )
25 dfss4 ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ⊆ ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) = ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) )
26 24 25 sylib ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) = ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) )
27 id ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ )
28 elfvdm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
29 28 difexd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑘 ) ) ∈ V )
30 29 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑘 ) ) ∈ V )
31 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑘 ) )
32 31 difeq2d ⊢ ( 𝑥 = 𝑘 → ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) = ( 𝑋 ∖ ( 𝑀 ‘ 𝑘 ) ) )
33 eqid ⊢ ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) )
34 32 33 fvmptg ⊢ ( ( 𝑘 ∈ ℕ ∧ ( 𝑋 ∖ ( 𝑀 ‘ 𝑘 ) ) ∈ V ) → ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑋 ∖ ( 𝑀 ‘ 𝑘 ) ) )
35 27 30 34 syl2anr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑋 ∖ ( 𝑀 ‘ 𝑘 ) ) )
36 15 difeq1d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑘 ) ) = ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) )
37 35 36 eqtrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) )
38 37 fveq2d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) )
39 26 38 eqtr4d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) = ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) )
40 39 eqeq1d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) = ∅ ↔ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ ) )
41 19 40 imbitrid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) = ∪ 𝐽 → ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ ) )
42 16 41 sylbid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = 𝑋 → ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ ) )
43 42 ralimdva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ∀ 𝑘 ∈ ℕ ( ( cls ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = 𝑋 → ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ ) )
44 4 43 sylan ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ∀ 𝑘 ∈ ℕ ( ( cls ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = 𝑋 → ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ ) )
45 ffvelcdm ⊢ ( ( 𝑀 : ℕ ⟶ 𝐽 ∧ 𝑥 ∈ ℕ ) → ( 𝑀 ‘ 𝑥 ) ∈ 𝐽 )
46 14 difeq1d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) = ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑥 ) ) )
47 46 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑀 ‘ 𝑥 ) ∈ 𝐽 ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) = ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑥 ) ) )
48 11 opncld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑀 ‘ 𝑥 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
49 5 48 sylan ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑀 ‘ 𝑥 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
50 47 49 eqeltrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑀 ‘ 𝑥 ) ∈ 𝐽 ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
51 45 50 sylan2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑀 : ℕ ⟶ 𝐽 ∧ 𝑥 ∈ ℕ ) ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
52 51 anassrs ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
53 52 ralrimiva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∀ 𝑥 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
54 4 53 sylan ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∀ 𝑥 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
55 33 fmpt ⊢ ( ∀ 𝑥 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
56 54 55 sylib ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
57 nne ⊢ ( ¬ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) ≠ ∅ ↔ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ )
58 57 ralbii ⊢ ( ∀ 𝑘 ∈ ℕ ¬ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) ≠ ∅ ↔ ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ )
59 ralnex ⊢ ( ∀ 𝑘 ∈ ℕ ¬ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) ≠ ∅ ↔ ¬ ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) ≠ ∅ )
60 58 59 bitr3i ⊢ ( ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ ↔ ¬ ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) ≠ ∅ )
61 1 bcth ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) ≠ ∅ ) → ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) ≠ ∅ )
62 61 3expia ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) → ( ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) ≠ ∅ → ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) ≠ ∅ ) )
63 62 necon1bd ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) → ( ¬ ∃ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) ≠ ∅ → ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) = ∅ ) )
64 60 63 biimtrid ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) → ( ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ → ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) = ∅ ) )
65 56 64 syldan ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ) = ∅ → ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) = ∅ ) )
66 difeq2 ⊢ ( ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) = ∅ → ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) ) = ( ∪ 𝐽 ∖ ∅ ) )
67 28 difexd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ V )
68 67 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ V )
69 68 ralrimiva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∀ 𝑥 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ V )
70 33 fnmpt ⊢ ( ∀ 𝑥 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ∈ V → ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) Fn ℕ )
71 fniunfv ⊢ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) Fn ℕ → ∪ 𝑘 ∈ ℕ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) )
72 69 70 71 3syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∪ 𝑘 ∈ ℕ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) )
73 35 iuneq2dv ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∪ 𝑘 ∈ ℕ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ∪ 𝑘 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑘 ) ) )
74 32 cbviunv ⊢ ∪ 𝑥 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) = ∪ 𝑘 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑘 ) )
75 73 74 eqtr4di ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∪ 𝑘 ∈ ℕ ( ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ∪ 𝑥 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) )
76 72 75 eqtr3d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) = ∪ 𝑥 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) )
77 iundif2 ⊢ ∪ 𝑥 ∈ ℕ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) = ( 𝑋 ∖ ∩ 𝑥 ∈ ℕ ( 𝑀 ‘ 𝑥 ) )
78 76 77 eqtrdi ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) = ( 𝑋 ∖ ∩ 𝑥 ∈ ℕ ( 𝑀 ‘ 𝑥 ) ) )
79 ffn ⊢ ( 𝑀 : ℕ ⟶ 𝐽 → 𝑀 Fn ℕ )
80 79 adantl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → 𝑀 Fn ℕ )
81 fniinfv ⊢ ( 𝑀 Fn ℕ → ∩ 𝑥 ∈ ℕ ( 𝑀 ‘ 𝑥 ) = ∩ ran 𝑀 )
82 80 81 syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∩ 𝑥 ∈ ℕ ( 𝑀 ‘ 𝑥 ) = ∩ ran 𝑀 )
83 82 difeq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( 𝑋 ∖ ∩ 𝑥 ∈ ℕ ( 𝑀 ‘ 𝑥 ) ) = ( 𝑋 ∖ ∩ ran 𝑀 ) )
84 14 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → 𝑋 = ∪ 𝐽 )
85 84 difeq1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( 𝑋 ∖ ∩ ran 𝑀 ) = ( ∪ 𝐽 ∖ ∩ ran 𝑀 ) )
86 78 83 85 3eqtrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) = ( ∪ 𝐽 ∖ ∩ ran 𝑀 ) )
87 86 fveq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) = ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ∩ ran 𝑀 ) ) )
88 87 difeq2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) ) = ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ∩ ran 𝑀 ) ) ) )
89 5 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → 𝐽 ∈ Top )
90 1nn ⊢ 1 ∈ ℕ
91 biidd ⊢ ( 𝑘 = 1 → ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∩ ran 𝑀 ⊆ ∪ 𝐽 ) ↔ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∩ ran 𝑀 ⊆ ∪ 𝐽 ) ) )
92 fnfvelrn ⊢ ( ( 𝑀 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ 𝑘 ) ∈ ran 𝑀 )
93 80 92 sylan ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ 𝑘 ) ∈ ran 𝑀 )
94 intss1 ⊢ ( ( 𝑀 ‘ 𝑘 ) ∈ ran 𝑀 → ∩ ran 𝑀 ⊆ ( 𝑀 ‘ 𝑘 ) )
95 93 94 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ∩ ran 𝑀 ⊆ ( 𝑀 ‘ 𝑘 ) )
96 95 10 sstrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ∩ ran 𝑀 ⊆ ∪ 𝐽 )
97 96 expcom ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∩ ran 𝑀 ⊆ ∪ 𝐽 ) )
98 91 97 vtoclga ⊢ ( 1 ∈ ℕ → ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∩ ran 𝑀 ⊆ ∪ 𝐽 ) )
99 90 98 ax-mp ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ∩ ran 𝑀 ⊆ ∪ 𝐽 )
100 11 clsval2 ⊢ ( ( 𝐽 ∈ Top ∧ ∩ ran 𝑀 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑀 ) = ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ∩ ran 𝑀 ) ) ) )
101 89 99 100 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑀 ) = ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ( ∪ 𝐽 ∖ ∩ ran 𝑀 ) ) ) )
102 88 101 eqtr4d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) ) = ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑀 ) )
103 dif0 ⊢ ( ∪ 𝐽 ∖ ∅ ) = ∪ 𝐽
104 103 84 eqtr4id ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ∪ 𝐽 ∖ ∅ ) = 𝑋 )
105 102 104 eqeq12d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ( ∪ 𝐽 ∖ ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) ) = ( ∪ 𝐽 ∖ ∅ ) ↔ ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑀 ) = 𝑋 ) )
106 66 105 imbitrid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) = ∅ → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑀 ) = 𝑋 ) )
107 4 106 sylan ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ( ( int ‘ 𝐽 ) ‘ ∪ ran ( 𝑥 ∈ ℕ ↦ ( 𝑋 ∖ ( 𝑀 ‘ 𝑥 ) ) ) ) = ∅ → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑀 ) = 𝑋 ) )
108 44 65 107 3syld ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ) → ( ∀ 𝑘 ∈ ℕ ( ( cls ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = 𝑋 → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑀 ) = 𝑋 ) )
109 108 3impia ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑀 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( ( cls ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ∩ ran 𝑀 ) = 𝑋 )