Theorem pnfxr 8225

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 3369	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 8209	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 8149	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4532	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4271	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2302	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3775	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3222	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 8211	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2305	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2200  Vcvv 2800   ∪ cun 3196  𝒫 cpw 3650  {cpr 3668  ∪ cuni 3891  ℂcc 8023  ℝcr 8024  +∞cpnf 8204  -∞cmnf 8205  ℝ^*cxr 8206

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 4205  ax-pow 4262  ax-un 4528  ax-cnex 8116

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-uni 3892  df-pnf 8209  df-xr 8211

This theorem is referenced by:  pnfex  8226  pnfnemnf  8227  xnn0xr  9463  xrltnr  10007  ltpnf  10008  mnfltpnf  10013  pnfnlt  10015  pnfge  10017  xrlttri3  10025  xnn0dcle  10030  nltpnft  10042  xgepnf  10044  xrrebnd  10047  xrre  10048  xrre2  10049  xnegcl  10060  xaddf  10072  xaddval  10073  xaddpnf1  10074  xaddpnf2  10075  pnfaddmnf  10078  mnfaddpnf  10079  xrex  10084  xaddass2  10098  xltadd1  10104  xlt2add  10108  xsubge0  10109  xposdif  10110  xleaddadd  10115  elioc2  10164  elico2  10165  elicc2  10166  ioomax  10176  iccmax  10177  ioopos  10178  elioopnf  10195  elicopnf  10197  unirnioo  10201  elxrge0  10206  dfrp2  10516  elicore  10519  xqltnle  10520  hashinfom  11033  rexico  11775  xrmaxiflemcl  11799  xrmaxadd  11815  fprodge0  12191  fprodge1  12193  pcxcl  12877  pc2dvds  12896  pcadd  12906  xblpnfps  15115  xblpnf  15116  xblss2ps  15121  blssec  15155  blpnfctr  15156  reopnap  15263  blssioo  15270