blsscls2

Description: A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014)

	Ref	Expression
Hypotheses	mopni.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	blcld.3	⊢ 𝑆 = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 }
Assertion	blsscls2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) → 𝑆 ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		mopni.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		blcld.3	⊢ 𝑆 = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 }
3		simplr3	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑅 < 𝑇 )
4		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑧 ) ∈ ℝ^* )
5	4	ad4ant124	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑧 ) ∈ ℝ^* )
6		simplr1	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑅 ∈ ℝ^* )
7		simplr2	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑇 ∈ ℝ^* )
8		xrlelttr	⊢ ( ( ( 𝑃 𝐷 𝑧 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ) → ( ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ∧ 𝑅 < 𝑇 ) → ( 𝑃 𝐷 𝑧 ) < 𝑇 ) )
9	8	expcomd	⊢ ( ( ( 𝑃 𝐷 𝑧 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ) → ( 𝑅 < 𝑇 → ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 → ( 𝑃 𝐷 𝑧 ) < 𝑇 ) ) )
10	5 6 7 9	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑅 < 𝑇 → ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 → ( 𝑃 𝐷 𝑧 ) < 𝑇 ) ) )
11	3 10	mpd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 → ( 𝑃 𝐷 𝑧 ) < 𝑇 ) )
12		simp2	⊢ ( ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) → 𝑇 ∈ ℝ^* )
13		elbl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑇 ∈ ℝ^* ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) ↔ ( 𝑃 𝐷 𝑧 ) < 𝑇 ) )
14	13	an4s	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑇 ∈ ℝ^* ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) ↔ ( 𝑃 𝐷 𝑧 ) < 𝑇 ) )
15	12 14	sylanr1	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) ↔ ( 𝑃 𝐷 𝑧 ) < 𝑇 ) )
16	15	anassrs	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) ↔ ( 𝑃 𝐷 𝑧 ) < 𝑇 ) )
17	11 16	sylibrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 → 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) ) )
18	17	ralrimiva	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) → ∀ 𝑧 ∈ 𝑋 ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 → 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) ) )
19		rabss	⊢ ( { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 → 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) ) )
20	18 19	sylibr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) )
21	2 20	eqsstrid	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇 ) ) → 𝑆 ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑇 ) )

Metamath Proof Explorer

Theorem blsscls2

Proof