Theorem icossxr 13472

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

Syntax hints:   ⊆ wss 3951  (class class class)co 7431  ℝ^*cxr 11294   < clt 11295   ≤ cle 11296  [,)cico 13389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-xr 11299  df-ico 13393

This theorem is referenced by:  leordtvallem2  23219  leordtval2  23220  nmoffn  24732  nmofval  24735  nmogelb  24737  nmolb  24738  nmof  24740  icopnfhmeo  24974  elovolm  25510  ovolmge0  25512  ovolgelb  25515  ovollb2lem  25523  ovoliunlem1  25537  ovoliunlem2  25538  ovolscalem1  25548  ovolicc1  25551  ioombl1lem2  25594  ioombl1lem4  25596  uniioovol  25614  uniiccvol  25615  uniioombllem1  25616  uniioombllem2  25618  uniioombllem3  25620  uniioombllem6  25623  ply1degltdimlem  33673  esumpfinvallem  34075  esummulc1  34082  esummulc2  34083  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2gt0cn  37682  xralrple2  45365  icoub  45539  liminflelimsuplem  45790  elhoi  46557  hoidmvlelem5  46614  ovnhoilem1  46616  ovnhoilem2  46617  ovnhoi  46618