# 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$