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

Proof

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