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

Theorem metdseq0 23456
 Description: The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015.)
Hypotheses
Ref Expression
metdscn.f 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
metdscn.j 𝐽 = (MetOpen‘𝐷)
Assertion
Ref Expression
metdseq0 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → ((𝐹𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐷,𝑦   𝑦,𝐽   𝑥,𝑆,𝑦   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)   𝐽(𝑥)

Proof of Theorem metdseq0
Dummy variables 𝑟 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll1 1208 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → 𝐷 ∈ (∞Met‘𝑋))
2 simprl 769 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → 𝑧𝐽)
3 simprr 771 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → 𝐴𝑧)
4 metdscn.j . . . . . . . 8 𝐽 = (MetOpen‘𝐷)
54mopni2 23097 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝐽𝐴𝑧) → ∃𝑟 ∈ ℝ+ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
61, 2, 3, 5syl3anc 1367 . . . . . 6 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → ∃𝑟 ∈ ℝ+ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
7 simprr 771 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
87ssrind 4212 . . . . . . 7 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ⊆ (𝑧𝑆))
9 rpgt0 12395 . . . . . . . . . 10 (𝑟 ∈ ℝ+ → 0 < 𝑟)
10 0re 10637 . . . . . . . . . . 11 0 ∈ ℝ
11 rpre 12391 . . . . . . . . . . 11 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
12 ltnle 10714 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (0 < 𝑟 ↔ ¬ 𝑟 ≤ 0))
1310, 11, 12sylancr 589 . . . . . . . . . 10 (𝑟 ∈ ℝ+ → (0 < 𝑟 ↔ ¬ 𝑟 ≤ 0))
149, 13mpbid 234 . . . . . . . . 9 (𝑟 ∈ ℝ+ → ¬ 𝑟 ≤ 0)
1514ad2antrl 726 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ¬ 𝑟 ≤ 0)
16 simpllr 774 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝐹𝐴) = 0)
1716breq2d 5071 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ (𝐹𝐴) ↔ 𝑟 ≤ 0))
181adantr 483 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝐷 ∈ (∞Met‘𝑋))
19 simpl2 1188 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝑆𝑋)
2019ad2antrr 724 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝑆𝑋)
21 simpl3 1189 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐴𝑋)
2221ad2antrr 724 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝐴𝑋)
23 rpxr 12392 . . . . . . . . . . . . 13 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
2423ad2antrl 726 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝑟 ∈ ℝ*)
25 metdscn.f . . . . . . . . . . . . 13 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
2625metdsge 23451 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑟 ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
2718, 20, 22, 24, 26syl31anc 1369 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
2817, 27bitr3d 283 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ 0 ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
29 incom 4178 . . . . . . . . . . 11 (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆)
3029eqeq1i 2826 . . . . . . . . . 10 ((𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅ ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) = ∅)
3128, 30syl6bb 289 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ 0 ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) = ∅))
3231necon3bbid 3053 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (¬ 𝑟 ≤ 0 ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅))
3315, 32mpbid 234 . . . . . . 7 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅)
34 ssn0 4354 . . . . . . 7 ((((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ⊆ (𝑧𝑆) ∧ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅) → (𝑧𝑆) ≠ ∅)
358, 33, 34syl2anc 586 . . . . . 6 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑧𝑆) ≠ ∅)
366, 35rexlimddv 3291 . . . . 5 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → (𝑧𝑆) ≠ ∅)
3736expr 459 . . . 4 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ 𝑧𝐽) → (𝐴𝑧 → (𝑧𝑆) ≠ ∅))
3837ralrimiva 3182 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → ∀𝑧𝐽 (𝐴𝑧 → (𝑧𝑆) ≠ ∅))
394mopntopon 23043 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
40393ad2ant1 1129 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → 𝐽 ∈ (TopOn‘𝑋))
4140adantr 483 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐽 ∈ (TopOn‘𝑋))
42 topontop 21515 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
4341, 42syl 17 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐽 ∈ Top)
44 toponuni 21516 . . . . . 6 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
4541, 44syl 17 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝑋 = 𝐽)
4619, 45sseqtrd 4007 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝑆 𝐽)
4721, 45eleqtrd 2915 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐴 𝐽)
48 eqid 2821 . . . . 5 𝐽 = 𝐽
4948elcls 21675 . . . 4 ((𝐽 ∈ Top ∧ 𝑆 𝐽𝐴 𝐽) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑧𝐽 (𝐴𝑧 → (𝑧𝑆) ≠ ∅)))
5043, 46, 47, 49syl3anc 1367 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑧𝐽 (𝐴𝑧 → (𝑧𝑆) ≠ ∅)))
5138, 50mpbird 259 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
52 incom 4178 . . . . . . 7 ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) = (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴)))
5325metdsf 23450 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) → 𝐹:𝑋⟶(0[,]+∞))
5453ffvelrnda 6846 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ 𝐴𝑋) → (𝐹𝐴) ∈ (0[,]+∞))
55543impa 1106 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (𝐹𝐴) ∈ (0[,]+∞))
56 eliccxr 12817 . . . . . . . . . 10 ((𝐹𝐴) ∈ (0[,]+∞) → (𝐹𝐴) ∈ ℝ*)
5755, 56syl 17 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (𝐹𝐴) ∈ ℝ*)
5857xrleidd 12539 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (𝐹𝐴) ≤ (𝐹𝐴))
5925metdsge 23451 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) ∈ ℝ*) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
6057, 59mpdan 685 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
6158, 60mpbid 234 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅)
6252, 61syl5eq 2868 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) = ∅)
6362adantr 483 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) = ∅)
6440ad2antrr 724 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
6564, 42syl 17 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐽 ∈ Top)
66 simpll2 1209 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝑆𝑋)
6764, 44syl 17 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝑋 = 𝐽)
6866, 67sseqtrd 4007 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝑆 𝐽)
69 simplr 767 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
70 simpll1 1208 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
71 simpll3 1210 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐴𝑋)
7257ad2antrr 724 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → (𝐹𝐴) ∈ ℝ*)
734blopn 23104 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝐴) ∈ ℝ*) → (𝐴(ball‘𝐷)(𝐹𝐴)) ∈ 𝐽)
7470, 71, 72, 73syl3anc 1367 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → (𝐴(ball‘𝐷)(𝐹𝐴)) ∈ 𝐽)
75 simpr 487 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 0 < (𝐹𝐴))
76 xblcntr 23015 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋 ∧ ((𝐹𝐴) ∈ ℝ* ∧ 0 < (𝐹𝐴))) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹𝐴)))
7770, 71, 72, 75, 76syl112anc 1370 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹𝐴)))
7848clsndisj 21677 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑆 𝐽𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ ((𝐴(ball‘𝐷)(𝐹𝐴)) ∈ 𝐽𝐴 ∈ (𝐴(ball‘𝐷)(𝐹𝐴)))) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) ≠ ∅)
7965, 68, 69, 74, 77, 78syl32anc 1374 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) ≠ ∅)
8079ex 415 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (0 < (𝐹𝐴) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) ≠ ∅))
8180necon2bd 3032 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) = ∅ → ¬ 0 < (𝐹𝐴)))
8263, 81mpd 15 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ¬ 0 < (𝐹𝐴))
83 elxrge0 12839 . . . . . . . . 9 ((𝐹𝐴) ∈ (0[,]+∞) ↔ ((𝐹𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹𝐴)))
8483simprbi 499 . . . . . . . 8 ((𝐹𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹𝐴))
8555, 84syl 17 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → 0 ≤ (𝐹𝐴))
86 0xr 10682 . . . . . . . 8 0 ∈ ℝ*
87 xrleloe 12531 . . . . . . . 8 ((0 ∈ ℝ* ∧ (𝐹𝐴) ∈ ℝ*) → (0 ≤ (𝐹𝐴) ↔ (0 < (𝐹𝐴) ∨ 0 = (𝐹𝐴))))
8886, 57, 87sylancr 589 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (0 ≤ (𝐹𝐴) ↔ (0 < (𝐹𝐴) ∨ 0 = (𝐹𝐴))))
8985, 88mpbid 234 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (0 < (𝐹𝐴) ∨ 0 = (𝐹𝐴)))
9089adantr 483 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (0 < (𝐹𝐴) ∨ 0 = (𝐹𝐴)))
9190ord 860 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (¬ 0 < (𝐹𝐴) → 0 = (𝐹𝐴)))
9282, 91mpd 15 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 0 = (𝐹𝐴))
9392eqcomd 2827 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹𝐴) = 0)
9451, 93impbida 799 1 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → ((𝐹𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  ∃wrex 3139   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  ∪ cuni 4832   class class class wbr 5059   ↦ cmpt 5139  ran crn 5551  ‘cfv 6350  (class class class)co 7150  infcinf 8899  ℝcr 10530  0cc0 10531  +∞cpnf 10666  ℝ*cxr 10668   < clt 10669   ≤ cle 10670  ℝ+crp 12383  [,]cicc 12735  ∞Metcxmet 20524  ballcbl 20526  MetOpencmopn 20529  Topctop 21495  TopOnctopon 21512  clsccl 21620 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-iin 4915  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-sup 8900  df-inf 8901  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-n0 11892  df-z 11976  df-uz 12238  df-q 12343  df-rp 12384  df-xneg 12501  df-xadd 12502  df-xmul 12503  df-icc 12739  df-topgen 16711  df-psmet 20531  df-xmet 20532  df-bl 20534  df-mopn 20535  df-top 21496  df-topon 21513  df-bases 21548  df-cld 21621  df-ntr 21622  df-cls 21623 This theorem is referenced by:  metnrmlem1a  23460  lebnumlem1  23559
 Copyright terms: Public domain W3C validator