elxr - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > elxr		Unicode version

Theorem elxr 9790

Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)

**Assertion**
Ref	Expression
elxr	$\/$ $\/$

**Proof of Theorem elxr**
Step	Hyp	Ref	Expression
1		df-xr 8010	. . 3
2	1	eleq2i 2254	. 2
3		elun 3288	. 2 $\/$
4		pnfex 8025	. . . . 5
5		mnfxr 8028	. . . . . 6
6	5	elexi 2761	. . . . 5
7	4, 6	elpr2 3626	. . . 4 $\/$
8	7	orbi2i 763	. . 3 $\/$ $\/$ $\/$
9		3orass 982	. . 3 $\/$ $\/$ $\/$ $\/$
10	8, 9	bitr4i 187	. 2 $\/$ $\/$ $\/$
11	2, 3, 10	3bitri 206	1 $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wb 105 $\/$ wo 709 $\/$ w3o 978

wceq 1363

wcel 2158

cun 3139

cpr 3605

cr 7824

cpnf 8003

cmnf 8004

cxr 8005

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 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-pow 4186 ax-un 4445 ax-cnex 7916

This theorem depends on definitions: df-bi 117 df-3or 980 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-rex 2471 df-v 2751 df-un 3145 df-in 3147 df-ss 3154 df-pw 3589 df-sn 3610 df-pr 3611 df-uni 3822 df-pnf 8008 df-mnf 8009 df-xr 8010

This theorem is referenced by: xrnemnf 9791 xrnepnf 9792 xrltnr 9793 xrltnsym 9807 xrlttr 9809 xrltso 9810 xrlttri3 9811 nltpnft 9828 npnflt 9829 ngtmnft 9831 nmnfgt 9832 xrrebnd 9833 xnegcl 9846 xnegneg 9847 xltnegi 9849 xrpnfdc 9856 xrmnfdc 9857 xnegid 9873 xaddcom 9875 xaddid1 9876 xnegdi 9882 xleadd1a 9887 xltadd1 9890 xlt2add 9894 xsubge0 9895 xposdif 9896 xleaddadd 9901 qbtwnxr 10272 xrmaxiflemcl 11267 xrmaxifle 11268 xrmaxiflemab 11269 xrmaxiflemlub 11270 xrmaxltsup 11280 xrmaxadd 11283 xrbdtri 11298 isxmet2d 14201 blssioo 14398