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

Theorem metdseq0 24603
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 1211 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → 𝐷 ∈ (∞Met‘𝑋))
2 simprl 768 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → 𝑧𝐽)
3 simprr 770 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → 𝐴𝑧)
4 metdscn.j . . . . . . . 8 𝐽 = (MetOpen‘𝐷)
54mopni2 24235 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝐽𝐴𝑧) → ∃𝑟 ∈ ℝ+ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
61, 2, 3, 5syl3anc 1370 . . . . . 6 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → ∃𝑟 ∈ ℝ+ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
7 simprr 770 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
87ssrind 4235 . . . . . . 7 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ⊆ (𝑧𝑆))
9 rpgt0 12993 . . . . . . . . . 10 (𝑟 ∈ ℝ+ → 0 < 𝑟)
10 0re 11223 . . . . . . . . . . 11 0 ∈ ℝ
11 rpre 12989 . . . . . . . . . . 11 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
12 ltnle 11300 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (0 < 𝑟 ↔ ¬ 𝑟 ≤ 0))
1310, 11, 12sylancr 586 . . . . . . . . . 10 (𝑟 ∈ ℝ+ → (0 < 𝑟 ↔ ¬ 𝑟 ≤ 0))
149, 13mpbid 231 . . . . . . . . 9 (𝑟 ∈ ℝ+ → ¬ 𝑟 ≤ 0)
1514ad2antrl 725 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ¬ 𝑟 ≤ 0)
16 simpllr 773 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝐹𝐴) = 0)
1716breq2d 5160 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ (𝐹𝐴) ↔ 𝑟 ≤ 0))
181adantr 480 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝐷 ∈ (∞Met‘𝑋))
19 simpl2 1191 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝑆𝑋)
2019ad2antrr 723 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝑆𝑋)
21 simpl3 1192 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐴𝑋)
2221ad2antrr 723 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝐴𝑋)
23 rpxr 12990 . . . . . . . . . . . . 13 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
2423ad2antrl 725 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝑟 ∈ ℝ*)
25 metdscn.f . . . . . . . . . . . . 13 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
2625metdsge 24598 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑟 ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
2718, 20, 22, 24, 26syl31anc 1372 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
2817, 27bitr3d 281 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ 0 ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
29 incom 4201 . . . . . . . . . . 11 (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆)
3029eqeq1i 2736 . . . . . . . . . 10 ((𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅ ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) = ∅)
3128, 30bitrdi 287 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ 0 ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) = ∅))
3231necon3bbid 2977 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (¬ 𝑟 ≤ 0 ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅))
3315, 32mpbid 231 . . . . . . 7 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅)
34 ssn0 4400 . . . . . . 7 ((((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ⊆ (𝑧𝑆) ∧ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅) → (𝑧𝑆) ≠ ∅)
358, 33, 34syl2anc 583 . . . . . 6 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑧𝑆) ≠ ∅)
366, 35rexlimddv 3160 . . . . 5 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ (𝑧𝐽𝐴𝑧)) → (𝑧𝑆) ≠ ∅)
3736expr 456 . . . 4 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) ∧ 𝑧𝐽) → (𝐴𝑧 → (𝑧𝑆) ≠ ∅))
3837ralrimiva 3145 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → ∀𝑧𝐽 (𝐴𝑧 → (𝑧𝑆) ≠ ∅))
394mopntopon 24178 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
40393ad2ant1 1132 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → 𝐽 ∈ (TopOn‘𝑋))
4140adantr 480 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐽 ∈ (TopOn‘𝑋))
42 topontop 22648 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
4341, 42syl 17 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐽 ∈ Top)
44 toponuni 22649 . . . . . 6 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
4541, 44syl 17 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝑋 = 𝐽)
4619, 45sseqtrd 4022 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝑆 𝐽)
4721, 45eleqtrd 2834 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐴 𝐽)
48 eqid 2731 . . . . 5 𝐽 = 𝐽
4948elcls 22810 . . . 4 ((𝐽 ∈ Top ∧ 𝑆 𝐽𝐴 𝐽) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑧𝐽 (𝐴𝑧 → (𝑧𝑆) ≠ ∅)))
5043, 46, 47, 49syl3anc 1370 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑧𝐽 (𝐴𝑧 → (𝑧𝑆) ≠ ∅)))
5138, 50mpbird 257 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) = 0) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
52 incom 4201 . . . . . . 7 ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) = (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴)))
5325metdsf 24597 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) → 𝐹:𝑋⟶(0[,]+∞))
5453ffvelcdmda 7086 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ 𝐴𝑋) → (𝐹𝐴) ∈ (0[,]+∞))
55543impa 1109 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (𝐹𝐴) ∈ (0[,]+∞))
56 eliccxr 13419 . . . . . . . . . 10 ((𝐹𝐴) ∈ (0[,]+∞) → (𝐹𝐴) ∈ ℝ*)
5755, 56syl 17 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (𝐹𝐴) ∈ ℝ*)
5857xrleidd 13138 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (𝐹𝐴) ≤ (𝐹𝐴))
5925metdsge 24598 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) ∈ ℝ*) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
6057, 59mpdan 684 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
6158, 60mpbid 231 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅)
6252, 61eqtrid 2783 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) = ∅)
6362adantr 480 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) = ∅)
6440ad2antrr 723 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
6564, 42syl 17 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐽 ∈ Top)
66 simpll2 1212 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝑆𝑋)
6764, 44syl 17 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝑋 = 𝐽)
6866, 67sseqtrd 4022 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝑆 𝐽)
69 simplr 766 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
70 simpll1 1211 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
71 simpll3 1213 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐴𝑋)
7257ad2antrr 723 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → (𝐹𝐴) ∈ ℝ*)
734blopn 24242 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝐴) ∈ ℝ*) → (𝐴(ball‘𝐷)(𝐹𝐴)) ∈ 𝐽)
7470, 71, 72, 73syl3anc 1370 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → (𝐴(ball‘𝐷)(𝐹𝐴)) ∈ 𝐽)
75 simpr 484 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 0 < (𝐹𝐴))
76 xblcntr 24150 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋 ∧ ((𝐹𝐴) ∈ ℝ* ∧ 0 < (𝐹𝐴))) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹𝐴)))
7770, 71, 72, 75, 76syl112anc 1373 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹𝐴)))
7848clsndisj 22812 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑆 𝐽𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ ((𝐴(ball‘𝐷)(𝐹𝐴)) ∈ 𝐽𝐴 ∈ (𝐴(ball‘𝐷)(𝐹𝐴)))) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) ≠ ∅)
7965, 68, 69, 74, 77, 78syl32anc 1377 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹𝐴)) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) ≠ ∅)
8079ex 412 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (0 < (𝐹𝐴) → ((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) ≠ ∅))
8180necon2bd 2955 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((𝐴(ball‘𝐷)(𝐹𝐴)) ∩ 𝑆) = ∅ → ¬ 0 < (𝐹𝐴)))
8263, 81mpd 15 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ¬ 0 < (𝐹𝐴))
83 elxrge0 13441 . . . . . . . . 9 ((𝐹𝐴) ∈ (0[,]+∞) ↔ ((𝐹𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹𝐴)))
8483simprbi 496 . . . . . . . 8 ((𝐹𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹𝐴))
8555, 84syl 17 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → 0 ≤ (𝐹𝐴))
86 0xr 11268 . . . . . . . 8 0 ∈ ℝ*
87 xrleloe 13130 . . . . . . . 8 ((0 ∈ ℝ* ∧ (𝐹𝐴) ∈ ℝ*) → (0 ≤ (𝐹𝐴) ↔ (0 < (𝐹𝐴) ∨ 0 = (𝐹𝐴))))
8886, 57, 87sylancr 586 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (0 ≤ (𝐹𝐴) ↔ (0 < (𝐹𝐴) ∨ 0 = (𝐹𝐴))))
8985, 88mpbid 231 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → (0 < (𝐹𝐴) ∨ 0 = (𝐹𝐴)))
9089adantr 480 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (0 < (𝐹𝐴) ∨ 0 = (𝐹𝐴)))
9190ord 861 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (¬ 0 < (𝐹𝐴) → 0 = (𝐹𝐴)))
9282, 91mpd 15 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 0 = (𝐹𝐴))
9392eqcomd 2737 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹𝐴) = 0)
9451, 93impbida 798 1 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) → ((𝐹𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844  w3a 1086   = wceq 1540  wcel 2105  wne 2939  wral 3060  wrex 3069  cin 3947  wss 3948  c0 4322   cuni 4908   class class class wbr 5148  cmpt 5231  ran crn 5677  cfv 6543  (class class class)co 7412  infcinf 9442  cr 11115  0cc0 11116  +∞cpnf 11252  *cxr 11254   < clt 11255  cle 11256  +crp 12981  [,]cicc 13334  ∞Metcxmet 21133  ballcbl 21135  MetOpencmopn 21138  Topctop 22628  TopOnctopon 22645  clsccl 22755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-er 8709  df-map 8828  df-en 8946  df-dom 8947  df-sdom 8948  df-sup 9443  df-inf 9444  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-n0 12480  df-z 12566  df-uz 12830  df-q 12940  df-rp 12982  df-xneg 13099  df-xadd 13100  df-xmul 13101  df-icc 13338  df-topgen 17396  df-psmet 21140  df-xmet 21141  df-bl 21143  df-mopn 21144  df-top 22629  df-topon 22646  df-bases 22682  df-cld 22756  df-ntr 22757  df-cls 22758
This theorem is referenced by:  metnrmlem1a  24607  lebnumlem1  24720
  Copyright terms: Public domain W3C validator