Theorem pnfxr 5416

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 5410	. . . . . 6 |- +oo = P~U.CC
2		axcnex 5190	. . . . . . . 8 |- CC e. V
3	2	uniex 2834	. . . . . . 7 |- U.CC e. V
4	3	pwex 2713	. . . . . 6 |- P~U.CC e. V
5	1, 4	eqeltr 1520	. . . . 5 |- +oo e. V
6	5	pri1 2420	. . . 4 |- +oo e. {+oo, -oo}
7	6	olci 271	. . 3 |- (+oo e. RR \/ +oo e. {+oo, -oo})
8		elun 2144	. . 3 |- (+oo e. (RR u. {+oo, -oo}) <-> (+oo e. RR \/ +oo e. {+oo, -oo}))
9	7, 8	mpbir 190	. 2 |- +oo e. (RR u. {+oo, -oo})
10		df-xr 5412	. 2 |- RR* = (RR u. {+oo, -oo})
11	9, 10	eleqtrr 1523	1 |- +oo e. RR*

Syntax hints:   \/ wo 222   e. wcel 1105  Vcvv 1786   u. cun 2016  P~cpw 2372  {cpr 2381  U.cuni 2471  CCcc 5155  RRcr 5156  +oocpnf 5406  -oocmnf 5407  RR*cxr 5408

This theorem is referenced by:  ltxrt 5418  elxr 5459  ssxr 5464  xrltnrt 5465  ltpnft 5466  mnfltpnf 5468  pnfnltt 5470  pnfget 5472  nltpnftt 5490  xrret 5493  xrre2t 5494  xrsupsslem 5974  xrinfmsslem 5975  xrinfmss 5977  supxrpnf 5986  supxrunb1 5987  supxrunb2 5988  supxrbnd 5989  qbtwnxr 6168  elioc2t 6273  elico2t 6274  elicc2t 6275  ioomax 6276  ioopos 6277  ioossre 6279  unirnioo 6286  tgioolem 7801  isblo3i 8327  cdrci 8738  truni1 8743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-qs 4204  df-ni 4923  df-nq 4961  df-np 5009  df-nr 5090  df-c 5163  df-pnf 5410  df-xr 5412

Copyright terms: Public domain