Theorem icossxr 11748

Description: A closed-below, open-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.)

Assertion

Ref	Expression
icossxr	|- ( A [,) B ) C_ RR*

Proof of Theorem icossxr

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

Step	Hyp	Ref	Expression
1		df-ico 11670	. 2 |- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
2	1	ixxssxr 11676	1 |- ( A [,) B ) C_ RR*

Syntax hints:   C_ wss 3416  (class class class)co 6315   RR*cxr 9700   < clt 9701   <_ cle 9702   [,)cico 11666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-1st 6820  df-2nd 6821  df-xr 9705  df-ico 11670

This theorem is referenced by:  leordtvallem2  20276  leordtval2  20277  nmoffn  21765  nmofval  21768  nmogelb  21770  nmolb  21771  nmof  21773  nmoffnOLD  21786  nmofvalOLD  21787  nmogelbOLD  21789  nmolbOLD  21790  nmofOLD  21791  icopnfhmeo  22020  elovolm  22477  ovolmge0  22479  ovolgelb  22482  ovollb2lem  22490  ovoliunlem1  22504  ovoliunlem2  22505  ovolscalem1  22515  ovolicc1  22518  ioombl1lem2  22561  ioombl1lem4  22563  uniioovol  22585  uniiccvol  22586  uniioombllem1  22587  uniioombllem2  22589  uniioombllem2OLD  22590  uniioombllem3  22592  uniioombllem6  22595  esumpfinvallem  28944  esummulc1  28951  esummulc2  28952  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  itg2gt0cn  32042  xralrple2  37615  icoub  37665  elhoi  38402  hoidmvlelem5  38459  ovnhoilem1  38461  ovnhoilem2  38462  ovnhoi  38463