Theorem pnfxr 8207

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 3368	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 8191	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 8131	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4528	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4267	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2302	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3772	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3221	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 8193	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2305	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2200  Vcvv 2799   ∪ cun 3195  𝒫 cpw 3649  {cpr 3667  ∪ cuni 3888  ℂcc 8005  ℝcr 8006  +∞cpnf 8186  -∞cmnf 8187  ℝ^*cxr 8188

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-un 4524  ax-cnex 8098

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-uni 3889  df-pnf 8191  df-xr 8193

This theorem is referenced by:  pnfex  8208  pnfnemnf  8209  xnn0xr  9445  xrltnr  9983  ltpnf  9984  mnfltpnf  9989  pnfnlt  9991  pnfge  9993  xrlttri3  10001  xnn0dcle  10006  nltpnft  10018  xgepnf  10020  xrrebnd  10023  xrre  10024  xrre2  10025  xnegcl  10036  xaddf  10048  xaddval  10049  xaddpnf1  10050  xaddpnf2  10051  pnfaddmnf  10054  mnfaddpnf  10055  xrex  10060  xaddass2  10074  xltadd1  10080  xlt2add  10084  xsubge0  10085  xposdif  10086  xleaddadd  10091  elioc2  10140  elico2  10141  elicc2  10142  ioomax  10152  iccmax  10153  ioopos  10154  elioopnf  10171  elicopnf  10173  unirnioo  10177  elxrge0  10182  dfrp2  10491  elicore  10494  xqltnle  10495  hashinfom  11008  rexico  11740  xrmaxiflemcl  11764  xrmaxadd  11780  fprodge0  12156  fprodge1  12158  pcxcl  12842  pc2dvds  12861  pcadd  12871  xblpnfps  15080  xblpnf  15081  xblss2ps  15086  blssec  15120  blpnfctr  15121  reopnap  15228  blssioo  15235