Theorem elicopnf 13545

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 11334	. . 3 ⊢ +∞ ∈ ℝ*
2		elico2 13510	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞)))
3	1, 2	mpan2 704	. 2 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞)))
4		ltpnf 13218	. . . . 5 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞)
5	4	adantr 486	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 < +∞)
6	5	pm4.71i 569	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 < +∞))
7		df-3an 1105	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞) ↔ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 < +∞))
8	6, 7	bitr4i 281	. 2 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < +∞))
9	3, 8	bitr4di 292	1 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ (𝐴[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145   class class class wbr 5102  (class class class)co 7408  ℝcr 11170  +∞cpnf 11311  ℝ^*cxr 11313   < clt 11314   ≤ cle 11315  [,)cico 13447

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11227  ax-resscn 11228  ax-pre-lttri 11245  ax-pre-lttrn 11246

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11316  df-mnf 11317  df-xr 11318  df-ltxr 11319  df-le 11320  df-ico 13451

This theorem is used by:  elrege0  13554  rexico  15488  limsupgle  15611  limsupgre  15615  rlim3  15632  ello12  15650  lo1bdd2  15658  elo12  15661  lo1resb  15698  rlimresb  15699  o1resb  15700  lo1eq  15702  rlimeq  15703  rlimsqzlem  15783  o1fsum  15947  ovolicopnf  25806  dvfsumrlimge0  26311  dvfsumrlim  26312  dvfsumrlim2  26313  cxp2lim  27267  chebbnd1  27762  chtppilimlem1  27763  chtppilimlem2  27764  chtppilim  27765  chebbnd2  27767  chto1lb  27768  chpchtlim  27769  chpo1ub  27770  vmadivsumb  27773  dchrisumlema  27778  dchrisumlem2  27780  dchrisumlem3  27781  dchrmusumlema  27783  dchrmusum2  27784  dchrvmasumlem2  27788  dchrvmasumiflem1  27791  dchrisum0lema  27804  dchrisum0lem1b  27805  dchrisum0lem2a  27807  dchrisum0lem2  27808  2vmadivsumlem  27830  selbergb  27839  selberg2b  27842  chpdifbndlem1  27843  selberg3lem1  27847  selberg3lem2  27848  selberg4lem1  27850  pntrsumo1  27855  selbergsb  27865  pntrlog2bndlem3  27869  pntpbnd1  27876  pntpbnd2  27877  pntibndlem3  27882  pntlemn  27890  pntlem3  27899  pntleml  27901  pnt2  27903  uzssico  33309  itg2addnclem2  38510  ceilhalfnn  48332  elbigo2  49586  rege1logbrege0  49592  blennnelnn  49610  dignnld  49637