# Metamath Proof Explorer

## Theorem ixxss12

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

Ref Expression
Hypotheses ixx.1 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
ixxss12.2 ${⊢}{P}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{T}{z}\wedge {z}{U}{y}\right)\right\}\right)$
ixxss12.3 ${⊢}\left({A}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left({A}{W}{C}\wedge {C}{T}{w}\right)\to {A}{R}{w}\right)$
ixxss12.4 ${⊢}\left({w}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({w}{U}{D}\wedge {D}{X}{B}\right)\to {w}{S}{B}\right)$
Assertion ixxss12 ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\to {C}{P}{D}\subseteq {A}{O}{B}$

### Proof

Step Hyp Ref Expression
1 ixx.1 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
2 ixxss12.2 ${⊢}{P}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{T}{z}\wedge {z}{U}{y}\right)\right\}\right)$
3 ixxss12.3 ${⊢}\left({A}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left({A}{W}{C}\wedge {C}{T}{w}\right)\to {A}{R}{w}\right)$
4 ixxss12.4 ${⊢}\left({w}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({w}{U}{D}\wedge {D}{X}{B}\right)\to {w}{S}{B}\right)$
5 2 elixx3g ${⊢}{w}\in \left({C}{P}{D}\right)↔\left(\left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\wedge \left({C}{T}{w}\wedge {w}{U}{D}\right)\right)$
6 5 simplbi ${⊢}{w}\in \left({C}{P}{D}\right)\to \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)$
7 6 adantl ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)$
8 7 simp3d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {w}\in {ℝ}^{*}$
9 simplrl ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {A}{W}{C}$
10 5 simprbi ${⊢}{w}\in \left({C}{P}{D}\right)\to \left({C}{T}{w}\wedge {w}{U}{D}\right)$
11 10 adantl ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to \left({C}{T}{w}\wedge {w}{U}{D}\right)$
12 11 simpld ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {C}{T}{w}$
13 simplll ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {A}\in {ℝ}^{*}$
14 7 simp1d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {C}\in {ℝ}^{*}$
15 13 14 8 3 syl3anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to \left(\left({A}{W}{C}\wedge {C}{T}{w}\right)\to {A}{R}{w}\right)$
16 9 12 15 mp2and ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {A}{R}{w}$
17 11 simprd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {w}{U}{D}$
18 simplrr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {D}{X}{B}$
19 7 simp2d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {D}\in {ℝ}^{*}$
20 simpllr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {B}\in {ℝ}^{*}$
21 8 19 20 4 syl3anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to \left(\left({w}{U}{D}\wedge {D}{X}{B}\right)\to {w}{S}{B}\right)$
22 17 18 21 mp2and ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {w}{S}{B}$
23 1 elixx1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({w}\in \left({A}{O}{B}\right)↔\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)\right)$
24 23 ad2antrr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to \left({w}\in \left({A}{O}{B}\right)↔\left({w}\in {ℝ}^{*}\wedge {A}{R}{w}\wedge {w}{S}{B}\right)\right)$
25 8 16 22 24 mpbir3and ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\wedge {w}\in \left({C}{P}{D}\right)\right)\to {w}\in \left({A}{O}{B}\right)$
26 25 ex ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\to \left({w}\in \left({C}{P}{D}\right)\to {w}\in \left({A}{O}{B}\right)\right)$
27 26 ssrdv ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}{W}{C}\wedge {D}{X}{B}\right)\right)\to {C}{P}{D}\subseteq {A}{O}{B}$