Theorem pnfxr 5558

Description: Plus infinity belongs to the set of extended reals.

Assertion

Ref	Expression
pnfxr	|- +oo e. RR*

Proof of Theorem pnfxr

Step	Hyp	Ref	Expression
1		df-pnf 5552	. . . . . 6 |- +oo = P~U.CC
2		axcnex 5332	. . . . . . . 8 |- CC e. V
3	2	uniex 2926	. . . . . . 7 |- U.CC e. V
4	3	pwex 2801	. . . . . 6 |- P~U.CC e. V
5	1, 4	eqeltri 1591	. . . . 5 |- +oo e. V
6	5	prid1 2504	. . . 4 |- +oo e. { +oo, -oo}
7	6	olci 278	. . 3 |- ( +oo e. RR \/ +oo e. { +oo, -oo})
8		elun 2224	. . 3 |- ( +oo e. (RR u. { +oo, -oo}) <-> ( +oo e. RR \/ +oo e. { +oo, -oo}))
9	7, 8	mpbir 197	. 2 |- +oo e. (RR u. { +oo, -oo})
10		df-xr 5554	. 2 |- RR* = (RR u. { +oo, -oo})
11	9, 10	eleqtrri 1594	1 |- +oo e. RR*

Syntax hints:   \/ wo 229   e. wcel 999  Vcvv 1858   u. cun 2096  P~cpw 2453  {cpr 2462  U.cuni 2557  CCcc 5297  RRcr 5298   +oocpnf 5548   -oocmnf 5549  RR*cxr 5550

This theorem is referenced by:  ltxr 5560  elxr 5600  pnfnemnf 5601  ssxr 5605  xrltnr 5606  ltpnf 5607  mnfltpnf 5609  pnfnlt 5611  pnfge 5613  nltpnft 5631  xrre 5634  xrre2 5635  xrsupsslem 6158  xrinfmsslem 6159  xrinfmss 6161  supxrpnf 6170  supxrunb1 6171  supxrunb2 6172  supxrbnd 6173  qbtwnxr 6332  elioc2 6415  elico2 6416  elicc2 6417  ioomax 6418  ioopos 6419  unirnioo 6428  tgioolem 7999  isblo3i 8545  cdrci 10588  truni1 10593

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-qs 4324  df-ni 5065  df-nq 5103  df-np 5151  df-nr 5232  df-c 5305  df-pnf 5552  df-xr 5554

Copyright terms: Public domain