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*|xRzzSy
ixxss2.2 P=x*,y*z*|xRzzTy
ixxss2.3 w*B*C*wTBBWCwSC
Assertion ixxss2 C*BWCAPBAOC

Proof

Step Hyp Ref Expression
1 ixx.1 O=x*,y*z*|xRzzSy
2 ixxss2.2 P=x*,y*z*|xRzzTy
3 ixxss2.3 w*B*C*wTBBWCwSC
4 2 elixx3g wAPBA*B*w*ARwwTB
5 4 simplbi wAPBA*B*w*
6 5 adantl C*BWCwAPBA*B*w*
7 6 simp3d C*BWCwAPBw*
8 4 simprbi wAPBARwwTB
9 8 adantl C*BWCwAPBARwwTB
10 9 simpld C*BWCwAPBARw
11 9 simprd C*BWCwAPBwTB
12 simplr C*BWCwAPBBWC
13 6 simp2d C*BWCwAPBB*
14 simpll C*BWCwAPBC*
15 7 13 14 3 syl3anc C*BWCwAPBwTBBWCwSC
16 11 12 15 mp2and C*BWCwAPBwSC
17 6 simp1d C*BWCwAPBA*
18 1 elixx1 A*C*wAOCw*ARwwSC
19 17 14 18 syl2anc C*BWCwAPBwAOCw*ARwwSC
20 7 10 16 19 mpbir3and C*BWCwAPBwAOC
21 20 ex C*BWCwAPBwAOC
22 21 ssrdv C*BWCAPBAOC