Theorem icossxr 12471

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	⊢ (𝐴[,)𝐵) ⊆ ℝ*

Proof of Theorem icossxr

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ico 12394	. 2 ⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
2	1	ixxssxr 12400	1 ⊢ (𝐴[,)𝐵) ⊆ ℝ*

Syntax hints:   ⊆ wss 3715  (class class class)co 6814  ℝ^*cxr 10285   < clt 10286   ≤ cle 10287  [,)cico 12390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-1st 7334  df-2nd 7335  df-xr 10290  df-ico 12394

This theorem is referenced by:  leordtvallem2  21237  leordtval2  21238  nmoffn  22736  nmofval  22739  nmogelb  22741  nmolb  22742  nmof  22744  icopnfhmeo  22963  elovolm  23463  ovolmge0  23465  ovolgelb  23468  ovollb2lem  23476  ovoliunlem1  23490  ovoliunlem2  23491  ovolscalem1  23501  ovolicc1  23504  ioombl1lem2  23547  ioombl1lem4  23549  uniioovol  23567  uniiccvol  23568  uniioombllem1  23569  uniioombllem2  23571  uniioombllem3  23573  uniioombllem6  23576  esumpfinvallem  30466  esummulc1  30473  esummulc2  30474  mblfinlem3  33779  mblfinlem4  33780  ismblfin  33781  itg2gt0cn  33796  xralrple2  40086  icoub  40273  liminflelimsuplem  40528  elhoi  41280  hoidmvlelem5  41337  ovnhoilem1  41339  ovnhoilem2  41340  ovnhoi  41341