Theorem iccss 11691

Description: Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 20-Feb-2015.)

Assertion

Ref	Expression
iccss	|- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,] D ) C_ ( A [,] B ) )

Proof of Theorem iccss

Dummy variables x w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rexr 9672	. . 3 |- ( A e. RR -> A e. RR* )
2		rexr 9672	. . 3 |- ( B e. RR -> B e. RR* )
3	1, 2	anim12i 574	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A e. RR* /\ B e. RR* ) )
4		df-icc 11631	. . 3 |- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
5		xrletr 11444	. . 3 |- ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A <_ C /\ C <_ w ) -> A <_ w ) )
6		xrletr 11444	. . 3 |- ( ( w e. RR* /\ D e. RR* /\ B e. RR* ) -> ( ( w <_ D /\ D <_ B ) -> w <_ B ) )
7	4, 4, 5, 6	ixxss12 11644	. 2 |- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,] D ) C_ ( A [,] B ) )
8	3, 7	sylan 478	1 |- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,] D ) C_ ( A [,] B ) )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1890   C_ wss 3371   class class class wbr 4373  (class class class)co 6275   RRcr 9524   RR*cxr 9660   <_ cle 9662   [,]cicc 11627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582  ax-pre-lttri 9599  ax-pre-lttrn 9600

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-po 4732  df-so 4733  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6780  df-2nd 6781  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-icc 11631

This theorem is referenced by:  xrhmeo  21984  lebnumii  22007  pcoval1  22054  pcoval2  22057  ivthicc  22419  dyaddisjlem  22564  volsup2  22574  volcn  22575  mbfi1fseqlem5  22688  dvcvx  22983  dvfsumle  22984  dvfsumabs  22986  harmonicbnd3  23944  ppisval  24041  chtwordi  24094  ppiwordi  24100  chpub  24159  cvmliftlem2  30014  fourierdlem76  38102  fourierdlem103  38129  fourierdlem104  38130  fourierdlem107  38133  fourierdlem112  38138  salexct3  38257  salgensscntex  38259