Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  met1stc Structured version   Visualization version   GIF version

Theorem met1stc 23134
 Description: The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
Hypothesis
Ref Expression
methaus.1 𝐽 = (MetOpen‘𝐷)
Assertion
Ref Expression
met1stc (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ 1stω)

Proof of Theorem met1stc
Dummy variables 𝑛 𝑟 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 methaus.1 . . 3 𝐽 = (MetOpen‘𝐷)
21mopntop 23053 . 2 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
31mopnuni 23054 . . . . . 6 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
43eleq2d 2901 . . . . 5 (𝐷 ∈ (∞Met‘𝑋) → (𝑥𝑋𝑥 𝐽))
54biimpar 481 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 𝐽) → 𝑥𝑋)
6 simpll 766 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ 𝑛 ∈ ℕ) → 𝐷 ∈ (∞Met‘𝑋))
7 simplr 768 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ 𝑛 ∈ ℕ) → 𝑥𝑋)
8 nnrp 12400 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
98adantl 485 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+)
109rpreccld 12441 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ+)
1110rpxrd 12432 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ*)
121blopn 23113 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ (1 / 𝑛) ∈ ℝ*) → (𝑥(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
136, 7, 11, 12syl3anc 1368 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ 𝑛 ∈ ℕ) → (𝑥(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
1413fmpttd 6871 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) → (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))):ℕ⟶𝐽)
1514frnd 6511 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ⊆ 𝐽)
16 nnex 11643 . . . . . . . . 9 ℕ ∈ V
1716mptex 6978 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ∈ V
1817rnex 7613 . . . . . . 7 ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ∈ V
1918elpw 4527 . . . . . 6 (ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ∈ 𝒫 𝐽 ↔ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ⊆ 𝐽)
2015, 19sylibr 237 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ∈ 𝒫 𝐽)
21 omelon 9107 . . . . . . . . 9 ω ∈ On
22 nnenom 13355 . . . . . . . . . 10 ℕ ≈ ω
2322ensymi 8556 . . . . . . . . 9 ω ≈ ℕ
24 isnumi 9373 . . . . . . . . 9 ((ω ∈ On ∧ ω ≈ ℕ) → ℕ ∈ dom card)
2521, 23, 24mp2an 691 . . . . . . . 8 ℕ ∈ dom card
26 ovex 7183 . . . . . . . . . 10 (𝑥(ball‘𝐷)(1 / 𝑛)) ∈ V
27 eqid 2824 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) = (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))
2826, 27fnmpti 6481 . . . . . . . . 9 (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) Fn ℕ
29 dffn4 6588 . . . . . . . . 9 ((𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) Fn ℕ ↔ (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))):ℕ–onto→ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))))
3028, 29mpbi 233 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))):ℕ–onto→ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))
31 fodomnum 9482 . . . . . . . 8 (ℕ ∈ dom card → ((𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))):ℕ–onto→ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ℕ))
3225, 30, 31mp2 9 . . . . . . 7 ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ℕ
33 domentr 8565 . . . . . . 7 ((ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ℕ ∧ ℕ ≈ ω) → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω)
3432, 22, 33mp2an 691 . . . . . 6 ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω
3534a1i 11 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω)
36 simpll 766 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) → 𝐷 ∈ (∞Met‘𝑋))
37 simprl 770 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) → 𝑧𝐽)
38 simprr 772 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) → 𝑥𝑧)
391mopni2 23106 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝐽𝑥𝑧) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)
4036, 37, 38, 39syl3anc 1368 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)
41 simp-4l 782 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝐷 ∈ (∞Met‘𝑋))
42 simp-4r 783 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑥𝑋)
43 simprl 770 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑦 ∈ ℕ)
4443nnrpd 12429 . . . . . . . . . . . . 13 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑦 ∈ ℝ+)
4544rpreccld 12441 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) ∈ ℝ+)
46 blcntr 23026 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋 ∧ (1 / 𝑦) ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)))
4741, 42, 45, 46syl3anc 1368 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)))
4845rpxrd 12432 . . . . . . . . . . . . 13 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) ∈ ℝ*)
49 simplrl 776 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑟 ∈ ℝ+)
5049rpxrd 12432 . . . . . . . . . . . . 13 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑟 ∈ ℝ*)
51 nnrecre 11679 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (1 / 𝑦) ∈ ℝ)
5251ad2antrl 727 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) ∈ ℝ)
5349rpred 12431 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑟 ∈ ℝ)
54 simprr 772 . . . . . . . . . . . . . 14 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) < 𝑟)
5552, 53, 54ltled 10787 . . . . . . . . . . . . 13 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) ≤ 𝑟)
56 ssbl 23036 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ ((1 / 𝑦) ∈ ℝ*𝑟 ∈ ℝ*) ∧ (1 / 𝑦) ≤ 𝑟) → (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ (𝑥(ball‘𝐷)𝑟))
5741, 42, 48, 50, 55, 56syl221anc 1378 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ (𝑥(ball‘𝐷)𝑟))
58 simplrr 777 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)
5957, 58sstrd 3964 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧)
6047, 59jca 515 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧))
61 elrp 12391 . . . . . . . . . . . 12 (𝑟 ∈ ℝ+ ↔ (𝑟 ∈ ℝ ∧ 0 < 𝑟))
62 nnrecl 11895 . . . . . . . . . . . 12 ((𝑟 ∈ ℝ ∧ 0 < 𝑟) → ∃𝑦 ∈ ℕ (1 / 𝑦) < 𝑟)
6361, 62sylbi 220 . . . . . . . . . . 11 (𝑟 ∈ ℝ+ → ∃𝑦 ∈ ℕ (1 / 𝑦) < 𝑟)
6463ad2antrl 727 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < 𝑟)
6560, 64reximddv 3268 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) → ∃𝑦 ∈ ℕ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧))
6640, 65rexlimddv 3284 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) → ∃𝑦 ∈ ℕ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧))
67 ovexd 7185 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ 𝑦 ∈ ℕ) → (𝑥(ball‘𝐷)(1 / 𝑦)) ∈ V)
68 vex 3484 . . . . . . . . . 10 𝑤 ∈ V
69 oveq2 7158 . . . . . . . . . . . . 13 (𝑛 = 𝑦 → (1 / 𝑛) = (1 / 𝑦))
7069oveq2d 7166 . . . . . . . . . . . 12 (𝑛 = 𝑦 → (𝑥(ball‘𝐷)(1 / 𝑛)) = (𝑥(ball‘𝐷)(1 / 𝑦)))
7170cbvmptv 5156 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) = (𝑦 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑦)))
7271elrnmpt 5816 . . . . . . . . . 10 (𝑤 ∈ V → (𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ↔ ∃𝑦 ∈ ℕ 𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦))))
7368, 72mp1i 13 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) → (𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ↔ ∃𝑦 ∈ ℕ 𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦))))
74 eleq2 2904 . . . . . . . . . . 11 (𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦)) → (𝑥𝑤𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦))))
75 sseq1 3979 . . . . . . . . . . 11 (𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦)) → (𝑤𝑧 ↔ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧))
7674, 75anbi12d 633 . . . . . . . . . 10 (𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦)) → ((𝑥𝑤𝑤𝑧) ↔ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧)))
7776adantl 485 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) ∧ 𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦))) → ((𝑥𝑤𝑤𝑧) ↔ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧)))
7867, 73, 77rexxfr2d 5300 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥𝑤𝑤𝑧) ↔ ∃𝑦 ∈ ℕ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧)))
7966, 78mpbird 260 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑧𝐽𝑥𝑧)) → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥𝑤𝑤𝑧))
8079expr 460 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ 𝑧𝐽) → (𝑥𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥𝑤𝑤𝑧)))
8180ralrimiva 3177 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) → ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥𝑤𝑤𝑧)))
82 breq1 5056 . . . . . . 7 (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → (𝑦 ≼ ω ↔ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω))
83 rexeq 3398 . . . . . . . . 9 (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → (∃𝑤𝑦 (𝑥𝑤𝑤𝑧) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥𝑤𝑤𝑧)))
8483imbi2d 344 . . . . . . . 8 (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → ((𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ (𝑥𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥𝑤𝑤𝑧))))
8584ralbidv 3192 . . . . . . 7 (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → (∀𝑧𝐽 (𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)) ↔ ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥𝑤𝑤𝑧))))
8682, 85anbi12d 633 . . . . . 6 (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → ((𝑦 ≼ ω ∧ ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))) ↔ (ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω ∧ ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥𝑤𝑤𝑧)))))
8786rspcev 3610 . . . . 5 ((ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ∈ 𝒫 𝐽 ∧ (ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω ∧ ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥𝑤𝑤𝑧)))) → ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
8820, 35, 81, 87syl12anc 835 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) → ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
895, 88syldan 594 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 𝐽) → ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
9089ralrimiva 3177 . 2 (𝐷 ∈ (∞Met‘𝑋) → ∀𝑥 𝐽𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧))))
91 eqid 2824 . . 3 𝐽 = 𝐽
9291is1stc2 22053 . 2 (𝐽 ∈ 1stω ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧𝐽 (𝑥𝑧 → ∃𝑤𝑦 (𝑥𝑤𝑤𝑧)))))
932, 90, 92sylanbrc 586 1 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ 1stω)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2115  ∀wral 3133  ∃wrex 3134  Vcvv 3481   ⊆ wss 3920  𝒫 cpw 4523  ∪ cuni 4825   class class class wbr 5053   ↦ cmpt 5133  dom cdm 5543  ran crn 5544  Oncon0 6179   Fn wfn 6339  –onto→wfo 6342  ‘cfv 6344  (class class class)co 7150  ωcom 7575   ≈ cen 8503   ≼ cdom 8504  cardccrd 9362  ℝcr 10535  0cc0 10536  1c1 10537  ℝ*cxr 10673   < clt 10674   ≤ cle 10675   / cdiv 11296  ℕcn 11637  ℝ+crp 12389  ∞Metcxmet 20533  ballcbl 20535  MetOpencmopn 20538  Topctop 21504  1stωc1stc 22048 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7456  ax-inf2 9102  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613  ax-pre-sup 10614 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3483  df-sbc 3760  df-csb 3868  df-dif 3923  df-un 3925  df-in 3927  df-ss 3937  df-pss 3939  df-nul 4278  df-if 4452  df-pw 4525  df-sn 4552  df-pr 4554  df-tp 4556  df-op 4558  df-uni 4826  df-int 4864  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-isom 6353  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7576  df-1st 7685  df-2nd 7686  df-wrecs 7944  df-recs 8005  df-rdg 8043  df-er 8286  df-map 8405  df-en 8507  df-dom 8508  df-sdom 8509  df-sup 8904  df-inf 8905  df-card 9366  df-acn 9369  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-div 11297  df-nn 11638  df-2 11700  df-n0 11898  df-z 11982  df-uz 12244  df-q 12349  df-rp 12390  df-xneg 12507  df-xadd 12508  df-xmul 12509  df-topgen 16720  df-psmet 20540  df-xmet 20541  df-bl 20543  df-mopn 20544  df-top 21505  df-topon 21522  df-bases 21557  df-1stc 22050 This theorem is referenced by:  metelcls  23915  metcnp4  23920  metcn4  23921
 Copyright terms: Public domain W3C validator