Theorem pnfxr 7690

Description: Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)

Assertion

Ref	Expression
pnfxr	⊢ +∞ ∈ ℝ*

Proof of Theorem pnfxr

Step	Hyp	Ref	Expression
1		ssun2 3187	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 7674	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 7616	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4297	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4047	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2172	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3576	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3044	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 7676	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2175	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 1448  Vcvv 2641   ∪ cun 3019  𝒫 cpw 3457  {cpr 3475  ∪ cuni 3683  ℂcc 7498  ℝcr 7499  +∞cpnf 7669  -∞cmnf 7670  ℝ^*cxr 7671

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-un 4293  ax-cnex 7586

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-rex 2381  df-v 2643  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-uni 3684  df-pnf 7674  df-xr 7676

This theorem is referenced by:  pnfex  7691  pnfnemnf  7692  xnn0xr  8897  xrltnr  9407  ltpnf  9408  mnfltpnf  9412  pnfnlt  9414  pnfge  9416  xrlttri3  9424  nltpnft  9438  xgepnf  9440  xrrebnd  9443  xrre  9444  xrre2  9445  xnegcl  9456  xaddf  9468  xaddval  9469  xaddpnf1  9470  xaddpnf2  9471  pnfaddmnf  9474  mnfaddpnf  9475  xrex  9480  xaddass2  9494  xltadd1  9500  xlt2add  9504  xsubge0  9505  xposdif  9506  xleaddadd  9511  elioc2  9560  elico2  9561  elicc2  9562  ioomax  9572  iccmax  9573  ioopos  9574  elioopnf  9591  elicopnf  9593  unirnioo  9597  elxrge0  9602  hashinfom  10365  rexico  10833  xrmaxiflemcl  10853  xrmaxadd  10869  xblpnfps  12326  xblpnf  12327  xblss2ps  12332  blssec  12366  blpnfctr  12367  blssioo  12464