Theorem elicopnf 13122

Description: Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.)

Assertion

Ref	Expression
elicopnf	⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)))

Proof of Theorem elicopnf

Step	Hyp	Ref	Expression
1		pnfxr 10976	. . 3 ⊢ +∞ ∈ ℝ*
2		elico2 13088	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞)))
3	1, 2	mpan2 687	. 2 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞)))
4		ltpnf 12801	. . . . 5 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
5	4	adantr 480	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 < +∞)
6	5	pm4.71i 559	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 < +∞))
7		df-3an 1087	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 < +∞))
8	6, 7	bitr4i 277	. 2 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞))
9	3, 8	bitr4di 288	1 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   ∈ wcel 2107   class class class wbr 5075  (class class class)co 7260  ℝcr 10817  +∞cpnf 10953  ℝ^*cxr 10955   < clt 10956   ≤ cle 10957  [,)cico 13026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-cnex 10874  ax-resscn 10875  ax-pre-lttri 10892  ax-pre-lttrn 10893

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5485  df-po 5499  df-so 5500  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-ov 7263  df-oprab 7264  df-mpo 7265  df-er 8461  df-en 8697  df-dom 8698  df-sdom 8699  df-pnf 10958  df-mnf 10959  df-xr 10960  df-ltxr 10961  df-le 10962  df-ico 13030

This theorem is referenced by:  elrege0  13131  rexico  15009  limsupgle  15130  limsupgre  15134  rlim3  15151  ello12  15169  lo1bdd2  15177  elo12  15180  lo1resb  15217  rlimresb  15218  o1resb  15219  lo1eq  15221  rlimeq  15222  rlimsqzlem  15304  o1fsum  15469  ovolicopnf  24631  dvfsumrlimge0  25137  dvfsumrlim  25138  dvfsumrlim2  25139  cxp2lim  26069  chebbnd1  26563  chtppilimlem1  26564  chtppilimlem2  26565  chtppilim  26566  chebbnd2  26568  chto1lb  26569  chpchtlim  26570  chpo1ub  26571  vmadivsumb  26574  dchrisumlema  26579  dchrisumlem2  26581  dchrisumlem3  26582  dchrmusumlema  26584  dchrmusum2  26585  dchrvmasumlem2  26589  dchrvmasumiflem1  26592  dchrisum0lema  26605  dchrisum0lem1b  26606  dchrisum0lem2a  26608  dchrisum0lem2  26609  2vmadivsumlem  26631  selbergb  26640  selberg2b  26643  chpdifbndlem1  26644  selberg3lem1  26648  selberg3lem2  26649  selberg4lem1  26651  pntrsumo1  26656  selbergsb  26666  pntrlog2bndlem3  26670  pntpbnd1  26677  pntpbnd2  26678  pntibndlem3  26683  pntlemn  26691  pntlem3  26700  pntleml  26702  pnt2  26704  uzssico  31047  itg2addnclem2  35798  2xp3dxp2ge1d  40132  elbigo2  45828  rege1logbrege0  45834  blennnelnn  45852  dignnld  45879