Metamath Proof Explorer

Theorem met1stc

Description: The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis methaus.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion met1stc ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ 1stω )

Proof

Step Hyp Ref Expression
1 methaus.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
3 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
4 3 eleq2d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝐽 ) )
5 4 biimpar ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝑥 ∈ 𝑋 )
6 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7 simplr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ 𝑋 )
8 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
9 8 adantl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ+ )
10 9 rpreccld ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
11 10 rpxrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ* )
12 1 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 1 / 𝑛 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ 𝐽 )
13 6 7 11 12 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ 𝐽 )
14 13 fmpttd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) : ℕ ⟶ 𝐽 )
15 14 frnd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ⊆ 𝐽 )
16 nnex ⊢ ℕ ∈ V
17 16 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ∈ V
18 17 rnex ⊢ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ∈ V
19 18 elpw ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ∈ 𝒫 𝐽 ↔ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ⊆ 𝐽 )
20 15 19 sylibr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ∈ 𝒫 𝐽 )
21 omelon ⊢ ω ∈ On
22 nnenom ⊢ ℕ ≈ ω
23 22 ensymi ⊢ ω ≈ ℕ
24 isnumi ⊢ ( ( ω ∈ On ∧ ω ≈ ℕ ) → ℕ ∈ dom card )
25 21 23 24 mp2an ⊢ ℕ ∈ dom card
26 ovex ⊢ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ V
27 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) )
28 26 27 fnmpti ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) Fn ℕ
29 dffn4 ⊢ ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) Fn ℕ ↔ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) : ℕ –onto→ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) )
30 28 29 mpbi ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) : ℕ –onto→ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) )
31 fodomnum ⊢ ( ℕ ∈ dom card → ( ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) : ℕ –onto→ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) → ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ≼ ℕ ) )
32 25 30 31 mp2 ⊢ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ≼ ℕ
33 domentr ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ≼ ℕ ∧ ℕ ≈ ω ) → ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ≼ ω )
34 32 22 33 mp2an ⊢ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ≼ ω
35 34 a1i ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ≼ ω )
36 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
37 simprl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑧 ∈ 𝐽 )
38 simprr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑥 ∈ 𝑧 )
39 1 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 )
40 36 37 38 39 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 )
41 simp-4l ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
42 simp-4r ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → 𝑥 ∈ 𝑋 )
43 simprl ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → 𝑦 ∈ ℕ )
44 43 nnrpd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → 𝑦 ∈ ℝ+ )
45 44 rpreccld ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → ( 1 / 𝑦 ) ∈ ℝ+ )
46 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 1 / 𝑦 ) ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) )
47 41 42 45 46 syl3anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) )
48 45 rpxrd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → ( 1 / 𝑦 ) ∈ ℝ* )
49 simplrl ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → 𝑟 ∈ ℝ+ )
50 49 rpxrd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → 𝑟 ∈ ℝ* )
51 nnrecre ⊢ ( 𝑦 ∈ ℕ → ( 1 / 𝑦 ) ∈ ℝ )
52 51 ad2antrl ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → ( 1 / 𝑦 ) ∈ ℝ )
53 49 rpred ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → 𝑟 ∈ ℝ )
54 simprr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → ( 1 / 𝑦 ) < 𝑟 )
55 52 53 54 ltled ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → ( 1 / 𝑦 ) ≤ 𝑟 )
56 ssbl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 1 / 𝑦 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) ∧ ( 1 / 𝑦 ) ≤ 𝑟 ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
57 41 42 48 50 55 56 syl221anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
58 simplrr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 )
59 57 58 sstrd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ 𝑧 )
60 47 59 jca ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) ∧ ( 𝑦 ∈ ℕ ∧ ( 1 / 𝑦 ) < 𝑟 ) ) → ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ 𝑧 ) )
61 elrp ⊢ ( 𝑟 ∈ ℝ+ ↔ ( 𝑟 ∈ ℝ ∧ 0 < 𝑟 ) )
62 nnrecl ⊢ ( ( 𝑟 ∈ ℝ ∧ 0 < 𝑟 ) → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < 𝑟 )
63 61 62 sylbi ⊢ ( 𝑟 ∈ ℝ+ → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < 𝑟 )
64 63 ad2antrl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ∃ 𝑦 ∈ ℕ ( 1 / 𝑦 ) < 𝑟 )
65 60 64 reximddv ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ∃ 𝑦 ∈ ℕ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ 𝑧 ) )
66 40 65 rexlimddv ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) → ∃ 𝑦 ∈ ℕ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ 𝑧 ) )
67 ovexd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ 𝑦 ∈ ℕ ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ∈ V )
68 vex ⊢ 𝑤 ∈ V
69 oveq2 ⊢ ( 𝑛 = 𝑦 → ( 1 / 𝑛 ) = ( 1 / 𝑦 ) )
70 69 oveq2d ⊢ ( 𝑛 = 𝑦 → ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) )
71 70 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) = ( 𝑦 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) )
72 71 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ↔ ∃ 𝑦 ∈ ℕ 𝑤 = ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ) )
73 68 72 mp1i ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) → ( 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ↔ ∃ 𝑦 ∈ ℕ 𝑤 = ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ) )
74 eleq2 ⊢ ( 𝑤 = ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ) )
75 sseq1 ⊢ ( 𝑤 = ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) → ( 𝑤 ⊆ 𝑧 ↔ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ 𝑧 ) )
76 74 75 anbi12d ⊢ ( 𝑤 = ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ 𝑧 ) ) )
77 76 adantl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) ∧ 𝑤 = ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ 𝑧 ) ) )
78 67 73 77 rexxfr2d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) → ( ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑦 ∈ ℕ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑦 ) ) ⊆ 𝑧 ) ) )
79 66 78 mpbird ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧 ) ) → ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
80 79 expr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
81 80 ralrimiva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
82 breq1 ⊢ ( 𝑦 = ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) → ( 𝑦 ≼ ω ↔ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ≼ ω ) )
83 rexeq ⊢ ( 𝑦 = ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) → ( ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
84 83 imbi2d ⊢ ( 𝑦 = ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) → ( ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
85 84 ralbidv ⊢ ( 𝑦 = ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
86 82 85 anbi12d ⊢ ( 𝑦 = ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) → ( ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ↔ ( ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
87 86 rspcev ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ∈ 𝒫 𝐽 ∧ ( ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑛 ∈ ℕ ↦ ( 𝑥 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) → ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
88 20 35 81 87 syl12anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
89 5 88 syldan ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
90 89 ralrimiva ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
91 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
92 91 is1stc2 ⊢ ( 𝐽 ∈ 1stω ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
93 2 90 92 sylanbrc ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ 1stω )