Theorem metdseq0 23459

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.

Step	Hyp	Ref	Expression
1		simpll1 1209	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → 𝐷 ∈ (∞Met‘𝑋))
2		simprl 770	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → 𝑧 ∈ 𝐽)
3		simprr 772	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → 𝐴 ∈ 𝑧)
4		metdscn.j	. . . . . . . 8 ⊢ 𝐽 = (MetOpen‘𝐷)
5	4	mopni2 23100	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧) → ∃𝑟 ∈ ℝ+ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
6	1, 2, 3, 5	syl3anc 1368	. . . . . 6 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → ∃𝑟 ∈ ℝ+ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
7		simprr 772	. . . . . . . 8 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
8	7	ssrind 4162	. . . . . . 7 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ⊆ (𝑧 ∩ 𝑆))
9		rpgt0 12389	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ+ → 0 < 𝑟)
10		0re 10632	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
11		rpre 12385	. . . . . . . . . . 11 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ)
12		ltnle 10709	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (0 < 𝑟 ↔ ¬ 𝑟 ≤ 0))
13	10, 11, 12	sylancr 590	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ+ → (0 < 𝑟 ↔ ¬ 𝑟 ≤ 0))
14	9, 13	mpbid 235	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ+ → ¬ 𝑟 ≤ 0)
15	14	ad2antrl 727	. . . . . . . 8 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ¬ 𝑟 ≤ 0)
16		simpllr 775	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝐹‘𝐴) = 0)
17	16	breq2d 5042	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ (𝐹‘𝐴) ↔ 𝑟 ≤ 0))
18	1	adantr 484	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝐷 ∈ (∞Met‘𝑋))
19		simpl2 1189	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝑆 ⊆ 𝑋)
20	19	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝑆 ⊆ 𝑋)
21		simpl3 1190	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐴 ∈ 𝑋)
22	21	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝐴 ∈ 𝑋)
23		rpxr 12386	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
24	23	ad2antrl 727	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝑟 ∈ ℝ*)
25		metdscn.f	. . . . . . . . . . . . 13 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
26	25	metdsge 23454	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑟 ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
27	18, 20, 22, 24, 26	syl31anc 1370	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
28	17, 27	bitr3d 284	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ 0 ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
29		incom 4128	. . . . . . . . . . 11 ⊢ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆)
30	29	eqeq1i 2803	. . . . . . . . . 10 ⊢ ((𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅ ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) = ∅)
31	28, 30	syl6bb 290	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ 0 ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) = ∅))
32	31	necon3bbid 3024	. . . . . . . 8 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (¬ 𝑟 ≤ 0 ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅))
33	15, 32	mpbid 235	. . . . . . 7 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅)
34		ssn0 4308	. . . . . . 7 ⊢ ((((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ⊆ (𝑧 ∩ 𝑆) ∧ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅) → (𝑧 ∩ 𝑆) ≠ ∅)
35	8, 33, 34	syl2anc 587	. . . . . 6 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑧 ∩ 𝑆) ≠ ∅)
36	6, 35	rexlimddv 3250	. . . . 5 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → (𝑧 ∩ 𝑆) ≠ ∅)
37	36	expr 460	. . . 4 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ 𝑧 ∈ 𝐽) → (𝐴 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))
38	37	ralrimiva 3149	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))
39	4	mopntopon 23046	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
40	39	3ad2ant1 1130	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
41	40	adantr 484	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐽 ∈ (TopOn‘𝑋))
42		topontop 21518	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
43	41, 42	syl 17	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐽 ∈ Top)
44		toponuni 21519	. . . . . 6 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
45	41, 44	syl 17	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝑋 = ∪ 𝐽)
46	19, 45	sseqtrd 3955	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝑆 ⊆ ∪ 𝐽)
47	21, 45	eleqtrd 2892	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐴 ∈ ∪ 𝐽)
48		eqid 2798	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
49	48	elcls 21678	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝐴 ∈ ∪ 𝐽) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅)))
50	43, 46, 47, 49	syl3anc 1368	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅)))
51	38, 50	mpbird 260	. 2 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
52		incom 4128	. . . . . . 7 ⊢ ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) = (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
53	25	metdsf 23453	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞))
54	53	ffvelrnda 6828	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ (0[,]+∞))
55	54	3impa 1107	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ (0[,]+∞))
56		eliccxr 12813	. . . . . . . . . 10 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → (𝐹‘𝐴) ∈ ℝ*)
57	55, 56	syl 17	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ ℝ*)
58	57	xrleidd 12533	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ≤ (𝐹‘𝐴))
59	25	metdsge 23454	. . . . . . . . 9 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅))
60	57, 59	mpdan 686	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅))
61	58, 60	mpbid 235	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)
62	52, 61	syl5eq 2845	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) = ∅)
63	62	adantr 484	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) = ∅)
64	40	ad2antrr 725	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
65	64, 42	syl 17	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐽 ∈ Top)
66		simpll2 1210	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝑆 ⊆ 𝑋)
67	64, 44	syl 17	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝑋 = ∪ 𝐽)
68	66, 67	sseqtrd 3955	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝑆 ⊆ ∪ 𝐽)
69		simplr 768	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
70		simpll1 1209	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
71		simpll3 1211	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ 𝑋)
72	57	ad2antrr 725	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → (𝐹‘𝐴) ∈ ℝ*)
73	4	blopn 23107	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝐴) ∈ ℝ*) → (𝐴(ball‘𝐷)(𝐹‘𝐴)) ∈ 𝐽)
74	70, 71, 72, 73	syl3anc 1368	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → (𝐴(ball‘𝐷)(𝐹‘𝐴)) ∈ 𝐽)
75		simpr 488	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 0 < (𝐹‘𝐴))
76		xblcntr 23018	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 < (𝐹‘𝐴))) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
77	70, 71, 72, 75, 76	syl112anc 1371	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
78	48	clsndisj 21680	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∈ 𝐽 ∧ 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴)))) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) ≠ ∅)
79	65, 68, 69, 74, 77, 78	syl32anc 1375	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) ≠ ∅)
80	79	ex 416	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (0 < (𝐹‘𝐴) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) ≠ ∅))
81	80	necon2bd 3003	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) = ∅ → ¬ 0 < (𝐹‘𝐴)))
82	63, 81	mpd 15	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ¬ 0 < (𝐹‘𝐴))
83		elxrge0 12835	. . . . . . . . 9 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) ↔ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹‘𝐴)))
84	83	simprbi 500	. . . . . . . 8 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐴))
85	55, 84	syl 17	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → 0 ≤ (𝐹‘𝐴))
86		0xr 10677	. . . . . . . 8 ⊢ 0 ∈ ℝ*
87		xrleloe 12525	. . . . . . . 8 ⊢ ((0 ∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → (0 ≤ (𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴))))
88	86, 57, 87	sylancr 590	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (0 ≤ (𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴))))
89	85, 88	mpbid 235	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))
90	89	adantr 484	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))
91	90	ord 861	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (¬ 0 < (𝐹‘𝐴) → 0 = (𝐹‘𝐴)))
92	82, 91	mpd 15	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 0 = (𝐹‘𝐴))
93	92	eqcomd 2804	. 2 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹‘𝐴) = 0)
94	51, 93	impbida 800	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ∪ cuni 4800   class class class wbr 5030   ↦ cmpt 5110  ran crn 5520  ‘cfv 6324  (class class class)co 7135  infcinf 8889  ℝcr 10525  0cc0 10526  +∞cpnf 10661  ℝ^*cxr 10663   < clt 10664   ≤ cle 10665  ℝ⁺crp 12377  [,]cicc 12729  ∞Metcxmet 20076  ballcbl 20078  MetOpencmopn 20081  Topctop 21498  TopOnctopon 21515  clsccl 21623

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604

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 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-sup 8890  df-inf 8891  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-icc 12733  df-topgen 16709  df-psmet 20083  df-xmet 20084  df-bl 20086  df-mopn 20087  df-top 21499  df-topon 21516  df-bases 21551  df-cld 21624  df-ntr 21625  df-cls 21626

This theorem is referenced by:  metnrmlem1a  23463  lebnumlem1  23566