blsscls2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > blsscls2		GIF version

Theorem blsscls2 14078

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

**Hypotheses**
Ref	Expression
mopni.1	⊢ 𝐽 = (MetOpen‘𝐷)
blcld.3	⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅}

**Assertion**
Ref	Expression
blsscls2	⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇))

Distinct variable groups: 𝑧,𝐷 𝑧,𝑅 𝑧,𝑃 𝑧,𝑇 𝑧,𝑋 Allowed substitution hints: 𝑆(𝑧) 𝐽(𝑧)

**Proof of Theorem blsscls2**
Step	Hyp	Ref	Expression
1		blcld.3	. 2 ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅}
2		simplr3 1041	. . . . . 6 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) ∧ 𝑧 ∈ 𝑋) → 𝑅 < 𝑇)
3		xmetcl 13937	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑃𝐷𝑧) ∈ ℝ^*)
4	3	3expa 1203	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑃𝐷𝑧) ∈ ℝ^*)
5	4	adantlr 477	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) ∧ 𝑧 ∈ 𝑋) → (𝑃𝐷𝑧) ∈ ℝ^*)
6		simplr1 1039	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) ∧ 𝑧 ∈ 𝑋) → 𝑅 ∈ ℝ^*)
7		simplr2 1040	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) ∧ 𝑧 ∈ 𝑋) → 𝑇 ∈ ℝ^*)
8		xrlelttr 9808	. . . . . . . 8 ⊢ (((𝑃𝐷𝑧) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^*) → (((𝑃𝐷𝑧) ≤ 𝑅 ∧ 𝑅 < 𝑇) → (𝑃𝐷𝑧) < 𝑇))
9	8	expcomd 1441	. . . . . . 7 ⊢ (((𝑃𝐷𝑧) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^*) → (𝑅 < 𝑇 → ((𝑃𝐷𝑧) ≤ 𝑅 → (𝑃𝐷𝑧) < 𝑇)))
10	5, 6, 7, 9	syl3anc 1238	. . . . . 6 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) ∧ 𝑧 ∈ 𝑋) → (𝑅 < 𝑇 → ((𝑃𝐷𝑧) ≤ 𝑅 → (𝑃𝐷𝑧) < 𝑇)))
11	2, 10	mpd 13	. . . . 5 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) ∧ 𝑧 ∈ 𝑋) → ((𝑃𝐷𝑧) ≤ 𝑅 → (𝑃𝐷𝑧) < 𝑇))
12		simp2 998	. . . . . . 7 ⊢ ((𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇) → 𝑇 ∈ ℝ^*)
13		elbl2 13978	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑇 ∈ ℝ^*) ∧ (𝑃 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧 ∈ (𝑃(ball‘𝐷)𝑇) ↔ (𝑃𝐷𝑧) < 𝑇))
14	13	an4s 588	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑇 ∈ ℝ^* ∧ 𝑧 ∈ 𝑋)) → (𝑧 ∈ (𝑃(ball‘𝐷)𝑇) ↔ (𝑃𝐷𝑧) < 𝑇))
15	12, 14	sylanr1 404	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ ((𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇) ∧ 𝑧 ∈ 𝑋)) → (𝑧 ∈ (𝑃(ball‘𝐷)𝑇) ↔ (𝑃𝐷𝑧) < 𝑇))
16	15	anassrs 400	. . . . 5 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (𝑃(ball‘𝐷)𝑇) ↔ (𝑃𝐷𝑧) < 𝑇))
17	11, 16	sylibrd 169	. . . 4 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) ∧ 𝑧 ∈ 𝑋) → ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝑃(ball‘𝐷)𝑇)))
18	17	ralrimiva 2550	. . 3 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) → ∀𝑧 ∈ 𝑋 ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝑃(ball‘𝐷)𝑇)))
19		rabss 3234	. . 3 ⊢ ({𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝑃(ball‘𝐷)𝑇) ↔ ∀𝑧 ∈ 𝑋 ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝑃(ball‘𝐷)𝑇)))
20	18, 19	sylibr 134	. 2 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) → {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝑃(ball‘𝐷)𝑇))
21	1, 20	eqsstrid 3203	1 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ^* ∧ 𝑇 ∈ ℝ^* ∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 978 = wceq 1353 ∈ wcel 2148 ∀wral 2455 {crab 2459 ⊆ wss 3131 class class class wbr 4005 ‘cfv 5218 (class class class)co 5877 ℝ^*cxr 7993 < clt 7994 ≤ cle 7995 ∞Metcxmet 13525 ballcbl 13527 MetOpencmopn 13530

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4123 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-cnex 7904 ax-resscn 7905 ax-pre-ltirr 7925 ax-pre-ltwlin 7926 ax-pre-lttrn 7927

This theorem depends on definitions: df-bi 117 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-iun 3890 df-br 4006 df-opab 4067 df-mpt 4068 df-id 4295 df-po 4298 df-iso 4299 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-fv 5226 df-ov 5880 df-oprab 5881 df-mpo 5882 df-1st 6143 df-2nd 6144 df-map 6652 df-pnf 7996 df-mnf 7997 df-xr 7998 df-ltxr 7999 df-le 8000 df-psmet 13532 df-xmet 13533 df-bl 13535

This theorem is referenced by: (None)

W3C validator