Theorem pnfxr 8342

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 3387	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 8326	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 8267	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4563	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4301	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2307	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3802	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3239	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 8328	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2310	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2205  Vcvv 2815   ∪ cun 3212  𝒫 cpw 3674  {cpr 3695  ∪ cuni 3919  ℂcc 8141  ℝcr 8142  +∞cpnf 8321  -∞cmnf 8322  ℝ^*cxr 8323

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-un 4559  ax-cnex 8234

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-uni 3920  df-pnf 8326  df-xr 8328

This theorem is referenced by:  pnfex  8343  pnfnemnf  8344  xnn0xr  9585  xrltnr  10131  ltpnf  10132  mnfltpnf  10137  pnfnlt  10139  pnfge  10141  xrlttri3  10149  xnn0dcle  10154  nltpnft  10166  xgepnf  10168  xrrebnd  10171  xrre  10172  xrre2  10173  xnegcl  10184  xaddf  10196  xaddval  10197  xaddpnf1  10198  xaddpnf2  10199  pnfaddmnf  10202  mnfaddpnf  10203  xrex  10208  xaddass2  10222  xltadd1  10228  xlt2add  10232  xsubge0  10233  xposdif  10234  xleaddadd  10239  elioc2  10288  elico2  10289  elicc2  10290  ioomax  10300  iccmax  10301  ioopos  10302  elioopnf  10319  elicopnf  10321  unirnioo  10325  elxrge0  10330  dfrp2  10647  elicore  10650  xqltnle  10651  hashinfom  11166  rexico  11931  xrmaxiflemcl  11955  xrmaxadd  11971  fprodge0  12348  fprodge1  12350  pcxcl  13034  pc2dvds  13053  pcadd  13063  xblpnfps  15375  xblpnf  15376  xblss2ps  15381  blssec  15415  blpnfctr  15416  reopnap  15523  blssioo  15530  repiecelem  16921  repiecele0  16922  repiecege0  16923