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  9588  xrltnr  10134  ltpnf  10135  mnfltpnf  10140  pnfnlt  10142  pnfge  10144  xrlttri3  10152  xnn0dcle  10157  nltpnft  10169  xgepnf  10171  xrrebnd  10174  xrre  10175  xrre2  10176  xnegcl  10187  xaddf  10199  xaddval  10200  xaddpnf1  10201  xaddpnf2  10202  pnfaddmnf  10205  mnfaddpnf  10206  xrex  10211  xaddass2  10225  xltadd1  10231  xlt2add  10235  xsubge0  10236  xposdif  10237  xleaddadd  10242  elioc2  10291  elico2  10292  elicc2  10293  ioomax  10303  iccmax  10304  ioopos  10305  elioopnf  10322  elicopnf  10324  unirnioo  10328  elxrge0  10333  dfrp2  10650  elicore  10653  xqltnle  10654  hashinfom  11169  rexico  11935  xrmaxiflemcl  11959  xrmaxadd  11975  fprodge0  12352  fprodge1  12354  pcxcl  13038  pc2dvds  13057  pcadd  13067  xblpnfps  15393  xblpnf  15394  xblss2ps  15399  blssec  15433  blpnfctr  15434  reopnap  15541  blssioo  15548  repiecelem  16949  repiecele0  16950  repiecege0  16951