Theorem metdstri 25084

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 785	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐹‘𝐴) ∈ ℝ)
2		simprl 783	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℝ)
3		rexsub 13289	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝐴) ∈ ℝ ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹‘𝐴) − (𝐴𝐷𝐵)))
4	1, 2, 3	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹‘𝐴) − (𝐴𝐷𝐵)))
5	4	oveq2d 7433	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = (𝐵(ball‘𝐷)((𝐹‘𝐴) − (𝐴𝐷𝐵))))
6		simpll 779	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐷 ∈ (∞Met‘𝑋))
7	6	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → 𝐷 ∈ (∞Met‘𝑋))
8		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐵 ∈ 𝑋)
9	8	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → 𝐵 ∈ 𝑋)
10		simprl 783	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐴 ∈ 𝑋)
11	10	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → 𝐴 ∈ 𝑋)
12	1, 2	resubcld 11670	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → ((𝐹‘𝐴) − (𝐴𝐷𝐵)) ∈ ℝ)
13	2	leidd 11808	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ≤ (𝐴𝐷𝐵))
14		xmetsym 24579	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
15	6, 10, 8, 14	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
16	15	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
17	16	eqcomd 2768	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵))
18	1	recnd 11265	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐹‘𝐴) ∈ ℂ)
19	2	recnd 11265	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℂ)
20	18, 19	nncand 11602	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → ((𝐹‘𝐴) − ((𝐹‘𝐴) − (𝐴𝐷𝐵))) = (𝐴𝐷𝐵))
21	13, 17, 20	3brtr4d 5141	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) ≤ ((𝐹‘𝐴) − ((𝐹‘𝐴) − (𝐴𝐷𝐵))))
22		blss2 24636	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (((𝐹‘𝐴) − (𝐴𝐷𝐵)) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐵𝐷𝐴) ≤ ((𝐹‘𝐴) − ((𝐹‘𝐴) − (𝐴𝐷𝐵))))) → (𝐵(ball‘𝐷)((𝐹‘𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
23	7, 9, 11, 12, 1, 21, 22	syl33anc 1412	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
24	5, 23	eqsstrd 3968	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
25	24	expr 462	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) ∈ ℝ → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))))
26	6	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐷 ∈ (∞Met‘𝑋))
27	8	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐵 ∈ 𝑋)
28		metdscn.f	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
29	28	metdsf 25081	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞))
30	29	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐹:𝑋⟶(0[,]+∞))
31	30, 10	ffvelcdmd 7082	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ∈ (0[,]+∞))
32		eliccxr 13492	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → (𝐹‘𝐴) ∈ ℝ*)
33	31, 32	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ∈ ℝ*)
34	33	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐹‘𝐴) ∈ ℝ*)
35		xmetcl 24563	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
36	6, 10, 8, 35	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ∈ ℝ*)
37	36	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐴𝐷𝐵) ∈ ℝ*)
38	37	xnegcld 13356	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
39	34, 38	xaddcld 13357	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
40	39	adantrr 730	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
41		pnfxr 11291	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ*
42	41	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → +∞ ∈ ℝ*)
43		pnfge 13185	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
44	40, 43	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
45		ssbl 24655	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋) ∧ (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
46	26, 27, 40, 42, 44, 45	syl221anc 1408	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
47		simprr 785	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐹‘𝐴) = +∞)
48	47	oveq2d 7433	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐴(ball‘𝐷)(𝐹‘𝐴)) = (𝐴(ball‘𝐷)+∞))
49	10	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐴 ∈ 𝑋)
50		simprl 783	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐴𝐷𝐵) ∈ ℝ)
51		xblpnf 24628	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
52	26, 49, 51	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
53	27, 50, 52	mpbir2and 726	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → 𝐵 ∈ (𝐴(ball‘𝐷)+∞))
54		blpnfctr 24668	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ (𝐴(ball‘𝐷)+∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
55	26, 49, 53, 54	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
56	48, 55	eqtr2d 2798	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵(ball‘𝐷)+∞) = (𝐴(ball‘𝐷)(𝐹‘𝐴)))
57	46, 56	sseqtrd 3970	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹‘𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
58	57	expr 462	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) = +∞ → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))))
59		elxrge0 13514	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) ↔ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹‘𝐴)))
60	59	simprbi 503	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐴))
61	31, 60	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 0 ≤ (𝐹‘𝐴))
62		ge0nemnf 13229	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹‘𝐴)) → (𝐹‘𝐴) ≠ -∞)
63	33, 61, 62	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≠ -∞)
64	33, 63	jca 521	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) ∈ ℝ* ∧ (𝐹‘𝐴) ≠ -∞))
65	64	adantr 486	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) ∈ ℝ* ∧ (𝐹‘𝐴) ≠ -∞))
66		xrnemnf 13172	. . . . . . . . 9 ⊢ (((𝐹‘𝐴) ∈ ℝ* ∧ (𝐹‘𝐴) ≠ -∞) ↔ ((𝐹‘𝐴) ∈ ℝ ∨ (𝐹‘𝐴) = +∞))
67	65, 66	sylib 221	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹‘𝐴) ∈ ℝ ∨ (𝐹‘𝐴) = +∞))
68	25, 58, 67	mpjaod 874	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
69		pnfnlt 13183	. . . . . . . . . . 11 ⊢ ((𝐹‘𝐴) ∈ ℝ* → ¬ +∞ < (𝐹‘𝐴))
70	33, 69	syl 18	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ¬ +∞ < (𝐹‘𝐴))
71	70	adantr 486	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ¬ +∞ < (𝐹‘𝐴))
72	36	xnegcld 13356	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
73	33, 72	xaddcld 13357	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
74		xbln0 24646	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋 ∧ ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
75	6, 8, 73, 74	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
76		xposdif 13318	. . . . . . . . . . . . 13 ⊢ (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐴𝐷𝐵) < (𝐹‘𝐴) ↔ 0 < ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
77	36, 33, 76	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵) < (𝐹‘𝐴) ↔ 0 < ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
78	75, 77	bitr4d 285	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ (𝐴𝐷𝐵) < (𝐹‘𝐴)))
79		breq1 5110	. . . . . . . . . . 11 ⊢ ((𝐴𝐷𝐵) = +∞ → ((𝐴𝐷𝐵) < (𝐹‘𝐴) ↔ +∞ < (𝐹‘𝐴)))
80	78, 79	sylan9bb 519	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ +∞ < (𝐹‘𝐴)))
81	80	necon1bbid 2996	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (¬ +∞ < (𝐹‘𝐴) ↔ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅))
82	71, 81	mpbid 235	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅)
83		0ss 4353	. . . . . . . 8 ⊢ ∅ ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴))
84	82, 83	eqsstrdi 3978	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
85		xmetge0 24576	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
86	6, 10, 8, 85	syl3anc 1398	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 0 ≤ (𝐴𝐷𝐵))
87		ge0nemnf 13229	. . . . . . . . . 10 ⊢ (((𝐴𝐷𝐵) ∈ ℝ* ∧ 0 ≤ (𝐴𝐷𝐵)) → (𝐴𝐷𝐵) ≠ -∞)
88	36, 86, 87	syl2anc 596	. . . . . . . . 9 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≠ -∞)
89	36, 88	jca 521	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞))
90		xrnemnf 13172	. . . . . . . 8 ⊢ (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞) ↔ ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
91	89, 90	sylib 221	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
92	68, 84, 91	mpjaodan 973	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)))
93		sslin 4191	. . . . . 6 ⊢ ((𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹‘𝐴)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))))
94	92, 93	syl 18	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))))
95	33	xrleidd 13207	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ (𝐹‘𝐴))
96		simplr 781	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝑆 ⊆ 𝑋)
97	28	metdsge 25082	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐹‘𝐴) ∈ ℝ*) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅))
98	6, 96, 10, 33, 97	syl31anc 1400	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅))
99	95, 98	mpbid 235	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅)
100		sseq0 4357	. . . . 5 ⊢ (((𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) ∧ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹‘𝐴))) = ∅) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
101	94, 99, 100	syl2anc 596	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
102	28	metdsge 25082	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
103	6, 96, 8, 73, 102	syl31anc 1400	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
104	101, 103	mpbird 260	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵))
105	30, 8	ffvelcdmd 7082	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐵) ∈ (0[,]+∞))
106		eliccxr 13492	. . . . 5 ⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) → (𝐹‘𝐵) ∈ ℝ*)
107	105, 106	syl 18	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐵) ∈ ℝ*)
108		elxrge0 13514	. . . . . 6 ⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) ↔ ((𝐹‘𝐵) ∈ ℝ* ∧ 0 ≤ (𝐹‘𝐵)))
109	108	simprbi 503	. . . . 5 ⊢ ((𝐹‘𝐵) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐵))
110	105, 109	syl 18	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 0 ≤ (𝐹‘𝐵))
111		xlesubadd 13319	. . . 4 ⊢ ((((𝐹‘𝐴) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹‘𝐵) ∈ ℝ*) ∧ (0 ≤ (𝐹‘𝐴) ∧ (𝐴𝐷𝐵) ≠ -∞ ∧ 0 ≤ (𝐹‘𝐵))) → (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝐹‘𝐴) ≤ ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵))))
112	33, 36, 107, 61, 88, 110, 111	syl33anc 1412	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (((𝐹‘𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹‘𝐵) ↔ (𝐹‘𝐴) ≤ ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵))))
113	104, 112	mpbid 235	. 2 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)))
114		xaddcom 13296	. . 3 ⊢ (((𝐹‘𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ*) → ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵)))
115	107, 36, 114	syl2anc 596	. 2 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵)))
116	113, 115	breqtrd 5135	1 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2957   ∩ cin 3901   ⊆ wss 3902  ∅c0 4282   class class class wbr 5107   ↦ cmpt 5190  ran crn 5660  ⟶wf 6533  ‘cfv 6537  (class class class)co 7417  infcinf 9415  ℝcr 11127  0cc0 11128  +∞cpnf 11268  -∞cmnf 11269  ℝ^*cxr 11270   < clt 11271   ≤ cle 11272   − cmin 11469  -_𝑒cxne 13164   +_𝑒 cxad 13165  [,]cicc 13405  ∞Metcxmet 21576  ballcbl 21578

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205  ax-pre-sup 11206

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-ec 8702  df-map 8832  df-en 8957  df-dom 8958  df-sdom 8959  df-sup 9416  df-inf 9417  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-div 11900  df-nn 12262  df-2 12331  df-rp 13047  df-xneg 13167  df-xadd 13168  df-xmul 13169  df-icc 13409  df-psmet 21583  df-xmet 21584  df-bl 21586

This theorem is used by:  metdsle  25085  metdscnlem  25088  metnrmlem1  25092