Theorem icossxr 13587

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

This proof depends on syntax axioms:   ⊆ wss 3900  (class class class)co 7440  ℝ^*cxr 11366   < clt 11367   ≤ cle 11368  [,)cico 13502

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-fv 6563  df-ov 7443  df-oprab 7444  df-mpo 7445  df-1st 8022  df-2nd 8023  df-xr 11371  df-ico 13506

This theorem is used by:  leordtvallem2  23556  leordtval2  23557  nmoffn  25057  nmofval  25060  nmogelb  25062  nmolb  25063  nmof  25065  icopnfhmeo  25291  elovolm  25823  ovolmge0  25825  ovolgelb  25828  ovollb2lem  25836  ovoliunlem1  25850  ovoliunlem2  25851  ovolscalem1  25861  ovolicc1  25864  ioombl1lem2  25907  ioombl1lem4  25909  uniioovol  25927  uniiccvol  25928  uniioombllem1  25929  uniioombllem2  25931  uniioombllem3  25933  uniioombllem6  25936  ply1degltdimlem  34321  esumpfinvallem  34773  esummulc1  34780  esummulc2  34781  mblfinlem3  38768  mblfinlem4  38769  ismblfin  38770  itg2gt0cn  38784  xralrple2  46569  icoub  46741  liminflelimsuplem  46988  elhoi  47755  hoidmvlelem5  47812  ovnhoilem1  47814  ovnhoilem2  47815  ovnhoi  47816