Theorem metdseq0 24750

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 1213	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → 𝐷 ∈ (∞Met‘𝑋))
2		simprl 770	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → 𝑧 ∈ 𝐽)
3		simprr 772	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → 𝐴 ∈ 𝑧)
4		metdscn.j	. . . . . . . 8 ⊢ 𝐽 = (MetOpen‘𝐷)
5	4	mopni2 24388	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧) → ∃𝑟 ∈ ℝ+ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
6	1, 2, 3, 5	syl3anc 1373	. . . . . 6 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → ∃𝑟 ∈ ℝ+ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
7		simprr 772	. . . . . . . 8 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)
8	7	ssrind 4210	. . . . . . 7 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ⊆ (𝑧 ∩ 𝑆))
9		rpgt0 12971	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ+ → 0 < 𝑟)
10		0re 11183	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
11		rpre 12967	. . . . . . . . . . 11 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ)
12		ltnle 11260	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (0 < 𝑟 ↔ ¬ 𝑟 ≤ 0))
13	10, 11, 12	sylancr 587	. . . . . . . . . 10 ⊢ (𝑟 ∈ ℝ+ → (0 < 𝑟 ↔ ¬ 𝑟 ≤ 0))
14	9, 13	mpbid 232	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ+ → ¬ 𝑟 ≤ 0)
15	14	ad2antrl 728	. . . . . . . 8 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ¬ 𝑟 ≤ 0)
16		simpllr 775	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝐹‘𝐴) = 0)
17	16	breq2d 5122	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ (𝐹‘𝐴) ↔ 𝑟 ≤ 0))
18	1	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝐷 ∈ (∞Met‘𝑋))
19		simpl2 1193	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝑆 ⊆ 𝑋)
20	19	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝑆 ⊆ 𝑋)
21		simpl3 1194	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐴 ∈ 𝑋)
22	21	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝐴 ∈ 𝑋)
23		rpxr 12968	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
24	23	ad2antrl 728	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → 𝑟 ∈ ℝ*)
25		metdscn.f	. . . . . . . . . . . . 13 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
26	25	metdsge 24745	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑟 ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
27	18, 20, 22, 24, 26	syl31anc 1375	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
28	17, 27	bitr3d 281	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ 0 ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅))
29		incom 4175	. . . . . . . . . . 11 ⊢ (𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆)
30	29	eqeq1i 2735	. . . . . . . . . 10 ⊢ ((𝑆 ∩ (𝐴(ball‘𝐷)𝑟)) = ∅ ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) = ∅)
31	28, 30	bitrdi 287	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑟 ≤ 0 ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) = ∅))
32	31	necon3bbid 2963	. . . . . . . 8 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (¬ 𝑟 ≤ 0 ↔ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅))
33	15, 32	mpbid 232	. . . . . . 7 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅)
34		ssn0 4370	. . . . . . 7 ⊢ ((((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ⊆ (𝑧 ∩ 𝑆) ∧ ((𝐴(ball‘𝐷)𝑟) ∩ 𝑆) ≠ ∅) → (𝑧 ∩ 𝑆) ≠ ∅)
35	8, 33, 34	syl2anc 584	. . . . . 6 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝐴(ball‘𝐷)𝑟) ⊆ 𝑧)) → (𝑧 ∩ 𝑆) ≠ ∅)
36	6, 35	rexlimddv 3141	. . . . 5 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ (𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧)) → (𝑧 ∩ 𝑆) ≠ ∅)
37	36	expr 456	. . . 4 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) ∧ 𝑧 ∈ 𝐽) → (𝐴 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))
38	37	ralrimiva 3126	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))
39	4	mopntopon 24334	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
40	39	3ad2ant1 1133	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
41	40	adantr 480	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐽 ∈ (TopOn‘𝑋))
42		topontop 22807	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
43	41, 42	syl 17	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐽 ∈ Top)
44		toponuni 22808	. . . . . 6 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
45	41, 44	syl 17	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝑋 = ∪ 𝐽)
46	19, 45	sseqtrd 3986	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝑆 ⊆ ∪ 𝐽)
47	21, 45	eleqtrd 2831	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐴 ∈ ∪ 𝐽)
48		eqid 2730	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
49	48	elcls 22967	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝐴 ∈ ∪ 𝐽) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅)))
50	43, 46, 47, 49	syl3anc 1373	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅)))
51	38, 50	mpbird 257	. 2 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) = 0) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
52		incom 4175	. . . . . . 7 ⊢ ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) = (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
53	25	metdsf 24744	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞))
54	53	ffvelcdmda 7059	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ (0[,]+∞))
55	54	3impa 1109	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ (0[,]+∞))
56		eliccxr 13403	. . . . . . . . . 10 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → (𝐹‘𝐴) ∈ ℝ*)
57	55, 56	syl 17	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ ℝ*)
58	57	xrleidd 13119	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ≤ (𝐹‘𝐴))
59	25	metdsge 24745	. . . . . . . . 9 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅))
60	57, 59	mpdan 687	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅))
61	58, 60	mpbid 232	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)
62	52, 61	eqtrid 2777	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) = ∅)
63	62	adantr 480	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) = ∅)
64	40	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
65	64, 42	syl 17	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐽 ∈ Top)
66		simpll2 1214	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝑆 ⊆ 𝑋)
67	64, 44	syl 17	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝑋 = ∪ 𝐽)
68	66, 67	sseqtrd 3986	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝑆 ⊆ ∪ 𝐽)
69		simplr 768	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ ((cls‘𝐽)‘𝑆))
70		simpll1 1213	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
71		simpll3 1215	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ 𝑋)
72	57	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → (𝐹‘𝐴) ∈ ℝ*)
73	4	blopn 24395	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ (𝐹‘𝐴) ∈ ℝ*) → (𝐴(ball‘𝐷)(𝐹‘𝐴)) ∈ 𝐽)
74	70, 71, 72, 73	syl3anc 1373	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → (𝐴(ball‘𝐷)(𝐹‘𝐴)) ∈ 𝐽)
75		simpr 484	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 0 < (𝐹‘𝐴))
76		xblcntr 24306	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 < (𝐹‘𝐴))) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
77	70, 71, 72, 75, 76	syl112anc 1376	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
78	48	clsndisj 22969	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∈ 𝐽 ∧ 𝐴 ∈ (𝐴(ball‘𝐷)(𝐹‘𝐴)))) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) ≠ ∅)
79	65, 68, 69, 74, 77, 78	syl32anc 1380	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) ∧ 0 < (𝐹‘𝐴)) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) ≠ ∅)
80	79	ex 412	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (0 < (𝐹‘𝐴) → ((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) ≠ ∅))
81	80	necon2bd 2942	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (((𝐴(ball‘𝐷)(𝐹‘𝐴)) ∩ 𝑆) = ∅ → ¬ 0 < (𝐹‘𝐴)))
82	63, 81	mpd 15	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → ¬ 0 < (𝐹‘𝐴))
83		elxrge0 13425	. . . . . . . . 9 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) ↔ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹‘𝐴)))
84	83	simprbi 496	. . . . . . . 8 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐴))
85	55, 84	syl 17	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → 0 ≤ (𝐹‘𝐴))
86		0xr 11228	. . . . . . . 8 ⊢ 0 ∈ ℝ*
87		xrleloe 13111	. . . . . . . 8 ⊢ ((0 ∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → (0 ≤ (𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴))))
88	86, 57, 87	sylancr 587	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (0 ≤ (𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴))))
89	85, 88	mpbid 232	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))
90	89	adantr 480	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))
91	90	ord 864	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (¬ 0 < (𝐹‘𝐴) → 0 = (𝐹‘𝐴)))
92	82, 91	mpd 15	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → 0 = (𝐹‘𝐴))
93	92	eqcomd 2736	. 2 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹‘𝐴) = 0)
94	51, 93	impbida 800	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  ∃wrex 3054   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  ∪ cuni 4874   class class class wbr 5110   ↦ cmpt 5191  ran crn 5642  ‘cfv 6514  (class class class)co 7390  infcinf 9399  ℝcr 11074  0cc0 11075  +∞cpnf 11212  ℝ^*cxr 11214   < clt 11215   ≤ cle 11216  ℝ⁺crp 12958  [,]cicc 13316  ∞Metcxmet 21256  ballcbl 21258  MetOpencmopn 21261  Topctop 22787  TopOnctopon 22804  clsccl 22912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-er 8674  df-map 8804  df-en 8922  df-dom 8923  df-sdom 8924  df-sup 9400  df-inf 9401  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-n0 12450  df-z 12537  df-uz 12801  df-q 12915  df-rp 12959  df-xneg 13079  df-xadd 13080  df-xmul 13081  df-icc 13320  df-topgen 17413  df-psmet 21263  df-xmet 21264  df-bl 21266  df-mopn 21267  df-top 22788  df-topon 22805  df-bases 22840  df-cld 22913  df-ntr 22914  df-cls 22915

This theorem is referenced by:  metnrmlem1a  24754  lebnumlem1  24867