Metamath Proof Explorer

Theorem ixxss2

Description: Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 ixx.1 ⊢ O = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x R z ∧ z S y
2 ixxss2.2 ⊢ P = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x R z ∧ z T y
3 ixxss2.3 ⊢ w ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → w T B ∧ B W C → w S C
4 2 elixx3g ⊢ w ∈ A P B ↔ A ∈ ℝ * ∧ B ∈ ℝ * ∧ w ∈ ℝ * ∧ A R w ∧ w T B
5 4 simplbi ⊢ w ∈ A P B → A ∈ ℝ * ∧ B ∈ ℝ * ∧ w ∈ ℝ *
6 5 adantl ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → A ∈ ℝ * ∧ B ∈ ℝ * ∧ w ∈ ℝ *
7 6 simp3d ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → w ∈ ℝ *
8 4 simprbi ⊢ w ∈ A P B → A R w ∧ w T B
9 8 adantl ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → A R w ∧ w T B
10 9 simpld ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → A R w
11 9 simprd ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → w T B
12 simplr ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → B W C
13 6 simp2d ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → B ∈ ℝ *
14 simpll ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → C ∈ ℝ *
15 7 13 14 3 syl3anc ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → w T B ∧ B W C → w S C
16 11 12 15 mp2and ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → w S C
17 6 simp1d ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → A ∈ ℝ *
18 1 elixx1 ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → w ∈ A O C ↔ w ∈ ℝ * ∧ A R w ∧ w S C
19 17 14 18 syl2anc ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → w ∈ A O C ↔ w ∈ ℝ * ∧ A R w ∧ w S C
20 7 10 16 19 mpbir3and ⊢ C ∈ ℝ * ∧ B W C ∧ w ∈ A P B → w ∈ A O C
21 20 ex ⊢ C ∈ ℝ * ∧ B W C → w ∈ A P B → w ∈ A O C
22 21 ssrdv ⊢ C ∈ ℝ * ∧ B W C → A P B ⊆ A O C