Theorem pnfxr 8012

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 3301	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 7996	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 7937	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4439	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4185	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2250	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3700	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3154	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 7998	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2253	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2148  Vcvv 2739   ∪ cun 3129  𝒫 cpw 3577  {cpr 3595  ∪ cuni 3811  ℂcc 7811  ℝcr 7812  +∞cpnf 7991  -∞cmnf 7992  ℝ^*cxr 7993

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-un 4435  ax-cnex 7904

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-uni 3812  df-pnf 7996  df-xr 7998

This theorem is referenced by:  pnfex  8013  pnfnemnf  8014  xnn0xr  9246  xrltnr  9781  ltpnf  9782  mnfltpnf  9787  pnfnlt  9789  pnfge  9791  xrlttri3  9799  xnn0dcle  9804  nltpnft  9816  xgepnf  9818  xrrebnd  9821  xrre  9822  xrre2  9823  xnegcl  9834  xaddf  9846  xaddval  9847  xaddpnf1  9848  xaddpnf2  9849  pnfaddmnf  9852  mnfaddpnf  9853  xrex  9858  xaddass2  9872  xltadd1  9878  xlt2add  9882  xsubge0  9883  xposdif  9884  xleaddadd  9889  elioc2  9938  elico2  9939  elicc2  9940  ioomax  9950  iccmax  9951  ioopos  9952  elioopnf  9969  elicopnf  9971  unirnioo  9975  elxrge0  9980  dfrp2  10266  elicore  10269  hashinfom  10760  rexico  11232  xrmaxiflemcl  11255  xrmaxadd  11271  fprodge0  11647  fprodge1  11649  pcxcl  12313  pc2dvds  12331  pcadd  12341  xblpnfps  13983  xblpnf  13984  xblss2ps  13989  blssec  14023  blpnfctr  14024  reopnap  14123  blssioo  14130