Theorem metdstri 22462

Description: A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol 𝑑 denotes the point-point and point-set distance functions, this theorem would be written 𝑑(𝑎, 𝑆) ≤ 𝑑(𝑎, 𝑏) + 𝑑(𝑏, 𝑆). (Contributed by Mario Carneiro, 4-Sep-2015.)

Hypothesis

Ref	Expression
metdscn.f	⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))

Assertion

Ref	Expression
metdstri	⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐷,𝑦   𝑥,𝐵,𝑦   𝑥,𝑆,𝑦   𝑥,𝑋,𝑦

Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem metdstri

Step	Hyp	Ref	Expression
1		simprr 792	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐹‘𝐴) ∈ ℝ)
2		simprl 790	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℝ)
3		rexsub 11938	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝐴) ∈ ℝ ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹‘𝐴) − (𝐴𝐷𝐵)))
4	1, 2, 3	syl2anc 691	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹‘𝐴) − (𝐴𝐷𝐵)))
5	4	oveq2d 6565	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = (𝐵(ball‘𝐷)((𝐹‘𝐴) − (𝐴𝐷𝐵))))
6		simpll 786	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐷 ∈ (∞Met‘𝑋))
7	6	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → 𝐷 ∈ (∞Met‘𝑋))
8		simprr 792	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐵 ∈ 𝑋)
9	8	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → 𝐵 ∈ 𝑋)
10		simprl 790	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐴 ∈ 𝑋)
11	10	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → 𝐴 ∈ 𝑋)
12	1, 2	resubcld 10337	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → ((𝐹‘𝐴) − (𝐴𝐷𝐵)) ∈ ℝ)
13	2	leidd 10473	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ≤ (𝐴𝐷𝐵))
14		xmetsym 21962	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
15	6, 10, 8, 14	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
16	15	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
17	16	eqcomd 2616	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵))
18	1	recnd 9947	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐹‘𝐴) ∈ ℂ)
19	2	recnd 9947	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℂ)
20	18, 19	nncand 10276	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → ((𝐹‘𝐴) − ((𝐹‘𝐴) − (𝐴𝐷𝐵))) = (𝐴𝐷𝐵))
21	13, 17, 20	3brtr4d 4615	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) ≤ ((𝐹‘𝐴) − ((𝐹‘𝐴) − (𝐴𝐷𝐵))))
22		blss2 22019	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (((𝐹‘𝐴) − (𝐴𝐷𝐵)) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐵𝐷𝐴) ≤ ((𝐹‘𝐴) − ((𝐹‘𝐴) − (𝐴𝐷𝐵))))) → (𝐵(ball‘𝐷)((𝐹‘𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
23	7, 9, 11, 12, 1, 21, 22	syl33anc 1333	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
24	5, 23	eqsstrd 3602	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
25	24	expr 641	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) ∈ ℝ → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))))
26	6	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐷 ∈ (∞Met‘𝑋))
27	8	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐵 ∈ 𝑋)
28		metdscn.f	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
29	28	metdsf 22459	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞))
30	29	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐹:𝑋⟶(0[,]+∞))
31	30, 10	ffvelrnd 6268	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ∈ (0[,]+∞))
32		elxrge0 12152	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) ↔ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹‘𝐴)))
33	32	simplbi 475	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → (𝐹‘𝐴) ∈ ℝ*)
34	31, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ∈ ℝ*)
35	34	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐹‘𝐴) ∈ ℝ*)
36		xmetcl 21946	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
37	6, 10, 8, 36	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ∈ ℝ*)
38	37	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐴𝐷𝐵) ∈ ℝ*)
39	38	xnegcld 12002	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
40	35, 39	xaddcld 12003	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
41	40	adantrr 749	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
42		pnfxr 9971	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ*
43	42	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → +∞ ∈ ℝ*)
44		pnfge 11840	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
45	41, 44	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
46		ssbl 22038	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋) ∧ (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
47	26, 27, 41, 43, 45, 46	syl221anc 1329	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
48		simprr 792	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐹‘𝐴) = +∞)
49	48	oveq2d 6565	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐴(ball‘𝐷)(𝐹‘𝐴)) = (𝐴(ball‘𝐷)+∞))
50	10	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐴 ∈ 𝑋)
51		simprl 790	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐴𝐷𝐵) ∈ ℝ)
52		xblpnf 22011	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
53	26, 50, 52	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
54	27, 51, 53	mpbir2and 959	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐵 ∈ (𝐴(ball‘𝐷)+∞))
55		blpnfctr 22051	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ (𝐴(ball‘𝐷)+∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
56	26, 50, 54, 55	syl3anc 1318	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
57	49, 56	eqtr2d 2645	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵(ball‘𝐷)+∞) = (𝐴(ball‘𝐷)(𝐹‘𝐴)))
58	47, 57	sseqtrd 3604	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
59	58	expr 641	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) = +∞ → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))))
60	32	simprbi 479	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐴))
61	31, 60	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 0 ≤ (𝐹‘𝐴))
62		ge0nemnf 11878	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹‘𝐴)) → (𝐹‘𝐴) ≠ -∞)
63	34, 61, 62	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≠ -∞)
64	34, 63	jca 553	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) ∈ ℝ* ∧ (𝐹‘𝐴) ≠ -∞))
65	64	adantr 480	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) ∈ ℝ* ∧ (𝐹‘𝐴) ≠ -∞))
66		xrnemnf 11827	. . . . . . . . 9 ⊢ (((𝐹‘𝐴) ∈ ℝ* ∧ (𝐹‘𝐴) ≠ -∞) ↔ ((𝐹‘𝐴) ∈ ℝ ∨ (𝐹‘𝐴) = +∞))
67	65, 66	sylib 207	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) ∈ ℝ ∨ (𝐹‘𝐴) = +∞))
68	25, 59, 67	mpjaod 395	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
69		pnfnlt 11838	. . . . . . . . . . 11 ⊢ ((𝐹‘𝐴) ∈ ℝ* → ¬ +∞ < (𝐹‘𝐴))
70	34, 69	syl 17	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ¬ +∞ < (𝐹‘𝐴))
71	70	adantr 480	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ¬ +∞ < (𝐹‘𝐴))
72	37	xnegcld 12002	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
73	34, 72	xaddcld 12003	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
74		xbln0 22029	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋 ∧ ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
75	6, 8, 73, 74	syl3anc 1318	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
76		xposdif 11964	. . . . . . . . . . . . 13 ⊢ (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐴𝐷𝐵) < (𝐹‘𝐴) ↔ 0 < ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
77	37, 34, 76	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵) < (𝐹‘𝐴) ↔ 0 < ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
78	75, 77	bitr4d 270	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ (𝐴𝐷𝐵) < (𝐹‘𝐴)))
79		breq1 4586	. . . . . . . . . . 11 ⊢ ((𝐴𝐷𝐵) = +∞ → ((𝐴𝐷𝐵) < (𝐹‘𝐴) ↔ +∞ < (𝐹‘𝐴)))
80	78, 79	sylan9bb 732	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ +∞ < (𝐹‘𝐴)))
81	80	necon1bbid 2821	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (¬ +∞ < (𝐹‘𝐴) ↔ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅))
82	71, 81	mpbid 221	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅)
83		0ss 3924	. . . . . . . 8 ⊢ ∅ ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))
84	82, 83	syl6eqss 3618	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
85		xmetge0 21959	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
86	6, 10, 8, 85	syl3anc 1318	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 0 ≤ (𝐴𝐷𝐵))
87		ge0nemnf 11878	. . . . . . . . . 10 ⊢ (((𝐴𝐷𝐵) ∈ ℝ* ∧ 0 ≤ (𝐴𝐷𝐵)) → (𝐴𝐷𝐵) ≠ -∞)
88	37, 86, 87	syl2anc 691	. . . . . . . . 9 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≠ -∞)
89	37, 88	jca 553	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞))
90		xrnemnf 11827	. . . . . . . 8 ⊢ (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞) ↔ ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
91	89, 90	sylib 207	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
92	68, 84, 91	mpjaodan 823	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
93		sslin 3801	. . . . . 6 ⊢ ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))))
94	92, 93	syl 17	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))))
95		xrleid 11859	. . . . . . 7 ⊢ ((𝐹‘𝐴) ∈ ℝ* → (𝐹‘𝐴) ≤ (𝐹‘𝐴))
96	34, 95	syl 17	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ (𝐹‘𝐴))
97		simplr 788	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝑆 ⊆ 𝑋)
98	28	metdsge 22460	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅))
99	6, 97, 10, 34, 98	syl31anc 1321	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅))
100	96, 99	mpbid 221	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)
101		sseq0 3927	. . . . 5 ⊢ (((𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) ∧ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
102	94, 100, 101	syl2anc 691	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
103	28	metdsge 22460	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
104	6, 97, 8, 73, 103	syl31anc 1321	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
105	102, 104	mpbird 246	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵))
106	30, 8	ffvelrnd 6268	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐵) ∈ (0[,]+∞))
107		elxrge0 12152	. . . . . 6 ⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) ↔ ((𝐹‘𝐵) ∈ ℝ* ∧ 0 ≤ (𝐹‘𝐵)))
108	107	simplbi 475	. . . . 5 ⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) → (𝐹‘𝐵) ∈ ℝ*)
109	106, 108	syl 17	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐵) ∈ ℝ*)
110	107	simprbi 479	. . . . 5 ⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐵))
111	106, 110	syl 17	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 0 ≤ (𝐹‘𝐵))
112		xlesubadd 11965	. . . 4 ⊢ ((((𝐹‘𝐴) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹‘𝐵) ∈ ℝ*) ∧ (0 ≤ (𝐹‘𝐴) ∧ (𝐴𝐷𝐵) ≠ -∞ ∧ 0 ≤ (𝐹‘𝐵))) → (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝐹‘𝐴) ≤ ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵))))
113	34, 37, 109, 61, 88, 111, 112	syl33anc 1333	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝐹‘𝐴) ≤ ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵))))
114	105, 113	mpbid 221	. 2 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)))
115		xaddcom 11945	. . 3 ⊢ (((𝐹‘𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ*) → ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵)))
116	109, 37, 115	syl2anc 691	. 2 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵)))
117	114, 116	breqtrd 4609	1 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   ↦ cmpt 4643  ran crn 5039  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  infcinf 8230  ℝcr 9814  0cc0 9815  +∞cpnf 9950  -∞cmnf 9951  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  -_𝑒cxne 11819   +_𝑒 cxad 11820  [,]cicc 12049  ∞Metcxmt 19552  ballcbl 19554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-er 7629  df-ec 7631  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-2 10956  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-icc 12053  df-psmet 19559  df-xmet 19560  df-bl 19562

This theorem is referenced by:  metdsle  22463  metdscnlem  22466  metnrmlem1  22470