Metamath Proof Explorer

Theorem ixxss1

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 ⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
ixxss1.2 ⊢ 𝑃 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑇 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
ixxss1.3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑇 𝑤 ) → 𝐴 𝑅 𝑤 ) )
Assertion ixxss1 ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) → ( 𝐵 𝑃 𝐶 ) ⊆ ( 𝐴 𝑂 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ixx.1 ⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2 ixxss1.2 ⊢ 𝑃 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑇 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
3 ixxss1.3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑇 𝑤 ) → 𝐴 𝑅 𝑤 ) )
4 2 elixx3g ⊢ ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ↔ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ∧ ( 𝐵 𝑇 𝑤 ∧ 𝑤 𝑆 𝐶 ) ) )
5 4 simplbi ⊢ ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) → ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) )
6 5 adantl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) )
7 6 simp3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝑤 ∈ ℝ* )
8 simplr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐴 𝑊 𝐵 )
9 4 simprbi ⊢ ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) → ( 𝐵 𝑇 𝑤 ∧ 𝑤 𝑆 𝐶 ) )
10 9 adantl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ( 𝐵 𝑇 𝑤 ∧ 𝑤 𝑆 𝐶 ) )
11 10 simpld ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐵 𝑇 𝑤 )
12 simpll ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐴 ∈ ℝ* )
13 6 simp1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐵 ∈ ℝ* )
14 12 13 7 3 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ( ( 𝐴 𝑊 𝐵 ∧ 𝐵 𝑇 𝑤 ) → 𝐴 𝑅 𝑤 ) )
15 8 11 14 mp2and ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐴 𝑅 𝑤 )
16 10 simprd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝑤 𝑆 𝐶 )
17 6 simp2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝐶 ∈ ℝ* )
18 1 elixx1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐶 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐶 ) ) )
19 12 17 18 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐶 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐶 ) ) )
20 7 15 16 19 mpbir3and ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) ∧ 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) ) → 𝑤 ∈ ( 𝐴 𝑂 𝐶 ) )
21 20 ex ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) → ( 𝑤 ∈ ( 𝐵 𝑃 𝐶 ) → 𝑤 ∈ ( 𝐴 𝑂 𝐶 ) ) )
22 21 ssrdv ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 𝑊 𝐵 ) → ( 𝐵 𝑃 𝐶 ) ⊆ ( 𝐴 𝑂 𝐶 ) )