Theorem pnfxr 8079

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 3327	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 8063	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 8003	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4472	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4216	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2269	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3728	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3180	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 8065	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2272	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2167  Vcvv 2763   ∪ cun 3155  𝒫 cpw 3605  {cpr 3623  ∪ cuni 3839  ℂcc 7877  ℝcr 7878  +∞cpnf 8058  -∞cmnf 8059  ℝ^*cxr 8060

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-un 4468  ax-cnex 7970

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-uni 3840  df-pnf 8063  df-xr 8065

This theorem is referenced by:  pnfex  8080  pnfnemnf  8081  xnn0xr  9317  xrltnr  9854  ltpnf  9855  mnfltpnf  9860  pnfnlt  9862  pnfge  9864  xrlttri3  9872  xnn0dcle  9877  nltpnft  9889  xgepnf  9891  xrrebnd  9894  xrre  9895  xrre2  9896  xnegcl  9907  xaddf  9919  xaddval  9920  xaddpnf1  9921  xaddpnf2  9922  pnfaddmnf  9925  mnfaddpnf  9926  xrex  9931  xaddass2  9945  xltadd1  9951  xlt2add  9955  xsubge0  9956  xposdif  9957  xleaddadd  9962  elioc2  10011  elico2  10012  elicc2  10013  ioomax  10023  iccmax  10024  ioopos  10025  elioopnf  10042  elicopnf  10044  unirnioo  10048  elxrge0  10053  dfrp2  10353  elicore  10356  xqltnle  10357  hashinfom  10870  rexico  11386  xrmaxiflemcl  11410  xrmaxadd  11426  fprodge0  11802  fprodge1  11804  pcxcl  12480  pc2dvds  12499  pcadd  12509  xblpnfps  14634  xblpnf  14635  xblss2ps  14640  blssec  14674  blpnfctr  14675  reopnap  14782  blssioo  14789