Theorem pnfxr 8215

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 3368	. . 3 ⊢ {+∞, -∞} ⊆ (ℝ ∪ {+∞, -∞})
2		df-pnf 8199	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3		cnex 8139	. . . . . . 7 ⊢ ℂ ∈ V
4	3	uniex 4529	. . . . . 6 ⊢ ∪ ℂ ∈ V
5	4	pwex 4268	. . . . 5 ⊢ 𝒫 ∪ ℂ ∈ V
6	2, 5	eqeltri 2302	. . . 4 ⊢ +∞ ∈ V
7	6	prid1 3772	. . 3 ⊢ +∞ ∈ {+∞, -∞}
8	1, 7	sselii 3221	. 2 ⊢ +∞ ∈ (ℝ ∪ {+∞, -∞})
9		df-xr 8201	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
10	8, 9	eleqtrri 2305	1 ⊢ +∞ ∈ ℝ*

Syntax hints:   ∈ wcel 2200  Vcvv 2799   ∪ cun 3195  𝒫 cpw 3649  {cpr 3667  ∪ cuni 3888  ℂcc 8013  ℝcr 8014  +∞cpnf 8194  -∞cmnf 8195  ℝ^*cxr 8196

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 4202  ax-pow 4259  ax-un 4525  ax-cnex 8106

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-uni 3889  df-pnf 8199  df-xr 8201

This theorem is referenced by:  pnfex  8216  pnfnemnf  8217  xnn0xr  9453  xrltnr  9992  ltpnf  9993  mnfltpnf  9998  pnfnlt  10000  pnfge  10002  xrlttri3  10010  xnn0dcle  10015  nltpnft  10027  xgepnf  10029  xrrebnd  10032  xrre  10033  xrre2  10034  xnegcl  10045  xaddf  10057  xaddval  10058  xaddpnf1  10059  xaddpnf2  10060  pnfaddmnf  10063  mnfaddpnf  10064  xrex  10069  xaddass2  10083  xltadd1  10089  xlt2add  10093  xsubge0  10094  xposdif  10095  xleaddadd  10100  elioc2  10149  elico2  10150  elicc2  10151  ioomax  10161  iccmax  10162  ioopos  10163  elioopnf  10180  elicopnf  10182  unirnioo  10186  elxrge0  10191  dfrp2  10500  elicore  10503  xqltnle  10504  hashinfom  11017  rexico  11753  xrmaxiflemcl  11777  xrmaxadd  11793  fprodge0  12169  fprodge1  12171  pcxcl  12855  pc2dvds  12874  pcadd  12884  xblpnfps  15093  xblpnf  15094  xblss2ps  15099  blssec  15133  blpnfctr  15134  reopnap  15241  blssioo  15248