Theorem pnfxr 7984

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 3297	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 7968	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 7910	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4431	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4178	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2248	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3695	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3150	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 7970	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2251	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2146  Vcvv 2735   ∪ cun 3125  𝒫 cpw 3572  {cpr 3590  ∪ cuni 3805  ℂcc 7784  ℝcr 7785  +∞cpnf 7963  -∞cmnf 7964  ℝ^*cxr 7965

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-un 4427  ax-cnex 7877

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-uni 3806  df-pnf 7968  df-xr 7970

This theorem is referenced by:  pnfex  7985  pnfnemnf  7986  xnn0xr  9217  xrltnr  9750  ltpnf  9751  mnfltpnf  9756  pnfnlt  9758  pnfge  9760  xrlttri3  9768  xnn0dcle  9773  nltpnft  9785  xgepnf  9787  xrrebnd  9790  xrre  9791  xrre2  9792  xnegcl  9803  xaddf  9815  xaddval  9816  xaddpnf1  9817  xaddpnf2  9818  pnfaddmnf  9821  mnfaddpnf  9822  xrex  9827  xaddass2  9841  xltadd1  9847  xlt2add  9851  xsubge0  9852  xposdif  9853  xleaddadd  9858  elioc2  9907  elico2  9908  elicc2  9909  ioomax  9919  iccmax  9920  ioopos  9921  elioopnf  9938  elicopnf  9940  unirnioo  9944  elxrge0  9949  dfrp2  10234  elicore  10237  hashinfom  10726  rexico  11198  xrmaxiflemcl  11221  xrmaxadd  11237  fprodge0  11613  fprodge1  11615  pcxcl  12278  pc2dvds  12296  pcadd  12306  xblpnfps  13478  xblpnf  13479  xblss2ps  13484  blssec  13518  blpnfctr  13519  reopnap  13618  blssioo  13625