Theorem elicopnf 13365

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 11190	. . 3 ⊢ +∞ ∈ ℝ*
2		elico2 13330	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞)))
3	1, 2	mpan2 692	. 2 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞)))
4		ltpnf 13038	. . . . 5 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
5	4	adantr 480	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 < +∞)
6	5	pm4.71i 559	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 < +∞))
7		df-3an 1089	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 < +∞))
8	6, 7	bitr4i 278	. 2 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞))
9	3, 8	bitr4di 289	1 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5099  (class class class)co 7360  ℝcr 11029  +∞cpnf 11167  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171  [,)cico 13267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-resscn 11087  ax-pre-lttri 11104  ax-pre-lttrn 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-ico 13271

This theorem is referenced by:  elrege0  13374  rexico  15281  limsupgle  15404  limsupgre  15408  rlim3  15425  ello12  15443  lo1bdd2  15451  elo12  15454  lo1resb  15491  rlimresb  15492  o1resb  15493  lo1eq  15495  rlimeq  15496  rlimsqzlem  15576  o1fsum  15740  ovolicopnf  25485  dvfsumrlimge0  25997  dvfsumrlim  25998  dvfsumrlim2  25999  cxp2lim  26947  chebbnd1  27443  chtppilimlem1  27444  chtppilimlem2  27445  chtppilim  27446  chebbnd2  27448  chto1lb  27449  chpchtlim  27450  chpo1ub  27451  vmadivsumb  27454  dchrisumlema  27459  dchrisumlem2  27461  dchrisumlem3  27462  dchrmusumlema  27464  dchrmusum2  27465  dchrvmasumlem2  27469  dchrvmasumiflem1  27472  dchrisum0lema  27485  dchrisum0lem1b  27486  dchrisum0lem2a  27488  dchrisum0lem2  27489  2vmadivsumlem  27511  selbergb  27520  selberg2b  27523  chpdifbndlem1  27524  selberg3lem1  27528  selberg3lem2  27529  selberg4lem1  27531  pntrsumo1  27536  selbergsb  27546  pntrlog2bndlem3  27550  pntpbnd1  27557  pntpbnd2  27558  pntibndlem3  27563  pntlemn  27571  pntlem3  27580  pntleml  27582  pnt2  27584  uzssico  32866  itg2addnclem2  37875  ceilhalfnn  47649  elbigo2  48865  rege1logbrege0  48871  blennnelnn  48889  dignnld  48916