| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ioossicc | Structured version Visualization version GIF version | ||
| Description: An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) |
| Ref | Expression |
|---|---|
| ioossicc | ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ioo 13391 | . 2 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | |
| 2 | df-icc 13394 | . 2 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) | |
| 3 | xrltle 13191 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴 ≤ 𝑤)) | |
| 4 | xrltle 13191 | . 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵)) | |
| 5 | 1, 2, 3, 4 | ixxssixx 13401 | 1 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
| Copyright terms: Public domain | W3C validator |