metdstri

Description: A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol d denotes the point-point and point-set distance functions, this theorem would be written d ( a , S ) <_ d ( a , b ) + d ( b , S ) . (Contributed by Mario Carneiro, 4-Sep-2015)

		Ref	Expression
	Hypothesis	metdscn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ^* , < ) )
	Assertion	metdstri	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +_𝑒 ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ^* , < ) )
2		simprr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
3		simprl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ )
4		rexsub	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) )
5	2 3 4	syl2anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) )
6	5	oveq2d	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) = ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) )
7		simpll	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8	7	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
9		simprr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
10	9	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → 𝐵 ∈ 𝑋 )
11		simprl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
12	11	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → 𝐴 ∈ 𝑋 )
13	2 3	resubcld	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ )
14	3	leidd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( 𝐴 𝐷 𝐵 ) )
15		xmetsym	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
16	7 11 9 15	syl3anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
17	16	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
18	17	eqcomd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) )
19	2	recnd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
20	3	recnd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℂ )
21	19 20	nncand	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) = ( 𝐴 𝐷 𝐵 ) )
22	14 18 21	3brtr4d	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 𝐷 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) )
23		blss2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐵 𝐷 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
24	8 10 12 13 2 22 23	syl33anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
25	6 24	eqsstrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
26	25	expr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) )
27	7	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
28	9	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → 𝐵 ∈ 𝑋 )
29	1	metdsf	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
30	29	adantr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
31	30 11	ffvelcdmd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
32		eliccxr	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* )
33	31 32	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* )
34	33	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* )
35		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* )
36	7 11 9 35	syl3anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* )
37	36	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* )
38	37	xnegcld	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → -_𝑒 ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* )
39	34 38	xaddcld	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ^* )
40	39	adantrr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ^* )
41		pnfxr	⊢ +∞ ∈ ℝ^*
42	41	a1i	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → +∞ ∈ ℝ^* )
43		pnfge	⊢ ( ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ^* → ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ +∞ )
44	40 43	syl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ +∞ )
45		ssbl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ) ∧ ( ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ^* ∧ +∞ ∈ ℝ^* ) ∧ ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ +∞ ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) )
46	27 28 40 42 44 45	syl221anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) )
47		simprr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐹 ‘ 𝐴 ) = +∞ )
48	47	oveq2d	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) = ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) )
49	11	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → 𝐴 ∈ 𝑋 )
50		simprl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ )
51		xblpnf	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ) )
52	27 49 51	syl2anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ) )
53	28 50 52	mpbir2and	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) )
54		blpnfctr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) ) → ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) = ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) )
55	27 49 53 54	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) = ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) )
56	48 55	eqtr2d	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) = ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
57	46 56	sseqtrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
58	57	expr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) = +∞ → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) )
59		elxrge0	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* ∧ 0 ≤ ( 𝐹 ‘ 𝐴 ) ) )
60	59	simprbi	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐹 ‘ 𝐴 ) )
61	31 60	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 0 ≤ ( 𝐹 ‘ 𝐴 ) )
62		ge0nemnf	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* ∧ 0 ≤ ( 𝐹 ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ≠ -∞ )
63	33 61 62	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ≠ -∞ )
64	33 63	jca	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* ∧ ( 𝐹 ‘ 𝐴 ) ≠ -∞ ) )
65	64	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* ∧ ( 𝐹 ‘ 𝐴 ) ≠ -∞ ) )
66		xrnemnf	⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* ∧ ( 𝐹 ‘ 𝐴 ) ≠ -∞ ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∨ ( 𝐹 ‘ 𝐴 ) = +∞ ) )
67	65 66	sylib	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∨ ( 𝐹 ‘ 𝐴 ) = +∞ ) )
68	26 58 67	mpjaod	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
69		pnfnlt	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* → ¬ +∞ < ( 𝐹 ‘ 𝐴 ) )
70	33 69	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ¬ +∞ < ( 𝐹 ‘ 𝐴 ) )
71	70	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ¬ +∞ < ( 𝐹 ‘ 𝐴 ) )
72	36	xnegcld	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → -_𝑒 ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* )
73	33 72	xaddcld	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ^* )
74		xbln0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ^* ) → ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ≠ ∅ ↔ 0 < ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) )
75	7 9 73 74	syl3anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ≠ ∅ ↔ 0 < ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) )
76		xposdif	⊢ ( ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* ) → ( ( 𝐴 𝐷 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ↔ 0 < ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) )
77	36 33 76	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ↔ 0 < ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) )
78	75 77	bitr4d	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ≠ ∅ ↔ ( 𝐴 𝐷 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ) )
79		breq1	⊢ ( ( 𝐴 𝐷 𝐵 ) = +∞ → ( ( 𝐴 𝐷 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ↔ +∞ < ( 𝐹 ‘ 𝐴 ) ) )
80	78 79	sylan9bb	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ≠ ∅ ↔ +∞ < ( 𝐹 ‘ 𝐴 ) ) )
81	80	necon1bbid	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ( ¬ +∞ < ( 𝐹 ‘ 𝐴 ) ↔ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) = ∅ ) )
82	71 81	mpbid	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) = ∅ )
83		0ss	⊢ ∅ ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) )
84	82 83	eqsstrdi	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
85		xmetge0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )
86	7 11 9 85	syl3anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )
87		ge0nemnf	⊢ ( ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* ∧ 0 ≤ ( 𝐴 𝐷 𝐵 ) ) → ( 𝐴 𝐷 𝐵 ) ≠ -∞ )
88	36 86 87	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≠ -∞ )
89	36 88	jca	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* ∧ ( 𝐴 𝐷 𝐵 ) ≠ -∞ ) )
90		xrnemnf	⊢ ( ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* ∧ ( 𝐴 𝐷 𝐵 ) ≠ -∞ ) ↔ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∨ ( 𝐴 𝐷 𝐵 ) = +∞ ) )
91	89 90	sylib	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∨ ( 𝐴 𝐷 𝐵 ) = +∞ ) )
92	68 84 91	mpjaodan	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
93		sslin	⊢ ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) → ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) ⊆ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) )
94	92 93	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) ⊆ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) )
95	33	xrleidd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) )
96		simplr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝑆 ⊆ 𝑋 )
97	1	metdsge	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* ) → ( ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) )
98	7 96 11 33 97	syl31anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) )
99	95 98	mpbid	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ )
100		sseq0	⊢ ( ( ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) ⊆ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) = ∅ )
101	94 99 100	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) = ∅ )
102	1	metdsge	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ^* ) → ( ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) = ∅ ) )
103	7 96 9 73 102	syl31anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) = ∅ ) )
104	101 103	mpbird	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) )
105	30 9	ffvelcdmd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
106		eliccxr	⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ^* )
107	105 106	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ^* )
108		elxrge0	⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ^* ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) )
109	108	simprbi	⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐹 ‘ 𝐵 ) )
110	105 109	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 0 ≤ ( 𝐹 ‘ 𝐵 ) )
111		xlesubadd	⊢ ( ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ^* ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ^* ) ∧ ( 0 ≤ ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐴 𝐷 𝐵 ) ≠ -∞ ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) ) → ( ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐵 ) +_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) )
112	33 36 107 61 88 110 111	syl33anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) +_𝑒 -_𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐵 ) +_𝑒 ( 𝐴 𝐷 𝐵 ) ) ) )
113	104 112	mpbid	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐵 ) +_𝑒 ( 𝐴 𝐷 𝐵 ) ) )
114		xaddcom	⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ^* ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ^* ) → ( ( 𝐹 ‘ 𝐵 ) +_𝑒 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) +_𝑒 ( 𝐹 ‘ 𝐵 ) ) )
115	107 36 114	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐵 ) +_𝑒 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) +_𝑒 ( 𝐹 ‘ 𝐵 ) ) )
116	113 115	breqtrd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +_𝑒 ( 𝐹 ‘ 𝐵 ) ) )

Metamath Proof Explorer

Theorem metdstri

Proof