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ω )