Theorem pnfxr 8138

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 3339	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 8122	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 8062	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4489	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4232	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2279	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3741	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3192	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 8124	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2282	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2177  Vcvv 2773   ∪ cun 3166  𝒫 cpw 3618  {cpr 3636  ∪ cuni 3853  ℂcc 7936  ℝcr 7937  +∞cpnf 8117  -∞cmnf 8118  ℝ^*cxr 8119

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4167  ax-pow 4223  ax-un 4485  ax-cnex 8029

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3172  df-in 3174  df-ss 3181  df-pw 3620  df-sn 3641  df-pr 3642  df-uni 3854  df-pnf 8122  df-xr 8124

This theorem is referenced by:  pnfex  8139  pnfnemnf  8140  xnn0xr  9376  xrltnr  9914  ltpnf  9915  mnfltpnf  9920  pnfnlt  9922  pnfge  9924  xrlttri3  9932  xnn0dcle  9937  nltpnft  9949  xgepnf  9951  xrrebnd  9954  xrre  9955  xrre2  9956  xnegcl  9967  xaddf  9979  xaddval  9980  xaddpnf1  9981  xaddpnf2  9982  pnfaddmnf  9985  mnfaddpnf  9986  xrex  9991  xaddass2  10005  xltadd1  10011  xlt2add  10015  xsubge0  10016  xposdif  10017  xleaddadd  10022  elioc2  10071  elico2  10072  elicc2  10073  ioomax  10083  iccmax  10084  ioopos  10085  elioopnf  10102  elicopnf  10104  unirnioo  10108  elxrge0  10113  dfrp2  10419  elicore  10422  xqltnle  10423  hashinfom  10936  rexico  11582  xrmaxiflemcl  11606  xrmaxadd  11622  fprodge0  11998  fprodge1  12000  pcxcl  12684  pc2dvds  12703  pcadd  12713  xblpnfps  14920  xblpnf  14921  xblss2ps  14926  blssec  14960  blpnfctr  14961  reopnap  15068  blssioo  15075