Metamath Proof Explorer

Theorem ixxssixx

Description: An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypotheses ixx.1 ⊢ O = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x R z ∧ z S y
ixx.2 ⊢ P = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x T z ∧ z U y
ixx.3 ⊢ A ∈ ℝ * ∧ w ∈ ℝ * → A R w → A T w
ixx.4 ⊢ w ∈ ℝ * ∧ B ∈ ℝ * → w S B → w U B
Assertion ixxssixx ⊢ A O B ⊆ A P B

Proof

Step Hyp Ref Expression
1 ixx.1 ⊢ O = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x R z ∧ z S y
2 ixx.2 ⊢ P = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x T z ∧ z U y
3 ixx.3 ⊢ A ∈ ℝ * ∧ w ∈ ℝ * → A R w → A T w
4 ixx.4 ⊢ w ∈ ℝ * ∧ B ∈ ℝ * → w S B → w U B
5 1 elmpocl ⊢ w ∈ A O B → A ∈ ℝ * ∧ B ∈ ℝ *
6 simp1 ⊢ w ∈ ℝ * ∧ A R w ∧ w S B → w ∈ ℝ *
7 6 a1i ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → w ∈ ℝ * ∧ A R w ∧ w S B → w ∈ ℝ *
8 simpl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ∈ ℝ *
9 3simpa ⊢ w ∈ ℝ * ∧ A R w ∧ w S B → w ∈ ℝ * ∧ A R w
10 3 expimpd ⊢ A ∈ ℝ * → w ∈ ℝ * ∧ A R w → A T w
11 8 9 10 syl2im ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → w ∈ ℝ * ∧ A R w ∧ w S B → A T w
12 simpr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B ∈ ℝ *
13 3simpb ⊢ w ∈ ℝ * ∧ A R w ∧ w S B → w ∈ ℝ * ∧ w S B
14 4 ancoms ⊢ B ∈ ℝ * ∧ w ∈ ℝ * → w S B → w U B
15 14 expimpd ⊢ B ∈ ℝ * → w ∈ ℝ * ∧ w S B → w U B
16 12 13 15 syl2im ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → w ∈ ℝ * ∧ A R w ∧ w S B → w U B
17 7 11 16 3jcad ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → w ∈ ℝ * ∧ A R w ∧ w S B → w ∈ ℝ * ∧ A T w ∧ w U B
18 1 elixx1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → w ∈ A O B ↔ w ∈ ℝ * ∧ A R w ∧ w S B
19 2 elixx1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → w ∈ A P B ↔ w ∈ ℝ * ∧ A T w ∧ w U B
20 17 18 19 3imtr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → w ∈ A O B → w ∈ A P B
21 5 20 mpcom ⊢ w ∈ A O B → w ∈ A P B
22 21 ssriv ⊢ A O B ⊆ A P B