Theorem pnfxr 8325

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 3382	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 8309	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 8250	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4557	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4295	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2305	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3796	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3234	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 8311	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2308	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2203  Vcvv 2812   ∪ cun 3208  𝒫 cpw 3668  {cpr 3689  ∪ cuni 3913  ℂcc 8124  ℝcr 8125  +∞cpnf 8304  -∞cmnf 8305  ℝ^*cxr 8306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-un 4553  ax-cnex 8217

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-uni 3914  df-pnf 8309  df-xr 8311

This theorem is referenced by:  pnfex  8326  pnfnemnf  8327  xnn0xr  9567  xrltnr  10111  ltpnf  10112  mnfltpnf  10117  pnfnlt  10119  pnfge  10121  xrlttri3  10129  xnn0dcle  10134  nltpnft  10146  xgepnf  10148  xrrebnd  10151  xrre  10152  xrre2  10153  xnegcl  10164  xaddf  10176  xaddval  10177  xaddpnf1  10178  xaddpnf2  10179  pnfaddmnf  10182  mnfaddpnf  10183  xrex  10188  xaddass2  10202  xltadd1  10208  xlt2add  10212  xsubge0  10213  xposdif  10214  xleaddadd  10219  elioc2  10268  elico2  10269  elicc2  10270  ioomax  10280  iccmax  10281  ioopos  10282  elioopnf  10299  elicopnf  10301  unirnioo  10305  elxrge0  10310  dfrp2  10622  elicore  10625  xqltnle  10626  hashinfom  11139  rexico  11902  xrmaxiflemcl  11926  xrmaxadd  11942  fprodge0  12319  fprodge1  12321  pcxcl  13005  pc2dvds  13024  pcadd  13034  xblpnfps  15255  xblpnf  15256  xblss2ps  15261  blssec  15295  blpnfctr  15296  reopnap  15403  blssioo  15410  repiecelem  16801  repiecele0  16802  repiecege0  16803