Theorem icossxr 13329

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 13248	. 2 ⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
2	1	ixxssxr 13254	1 ⊢ (𝐴[,)𝐵) ⊆ ℝ*

Syntax hints:   ⊆ wss 3902  (class class class)co 7346  ℝ^*cxr 11142   < clt 11143   ≤ cle 11144  [,)cico 13244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-cnex 11059  ax-resscn 11060

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-xr 11147  df-ico 13248

This theorem is referenced by:  leordtvallem2  23124  leordtval2  23125  nmoffn  24624  nmofval  24627  nmogelb  24629  nmolb  24630  nmof  24632  icopnfhmeo  24866  elovolm  25401  ovolmge0  25403  ovolgelb  25406  ovollb2lem  25414  ovoliunlem1  25428  ovoliunlem2  25429  ovolscalem1  25439  ovolicc1  25442  ioombl1lem2  25485  ioombl1lem4  25487  uniioovol  25505  uniiccvol  25506  uniioombllem1  25507  uniioombllem2  25509  uniioombllem3  25511  uniioombllem6  25514  ply1degltdimlem  33630  esumpfinvallem  34082  esummulc1  34089  esummulc2  34090  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  itg2gt0cn  37714  xralrple2  45392  icoub  45565  liminflelimsuplem  45812  elhoi  46579  hoidmvlelem5  46636  ovnhoilem1  46638  ovnhoilem2  46639  ovnhoi  46640