elxr - Intuitionistic Logic Explorer

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

Theorem elxr 9898

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 8111	. . 3
2	1	eleq2i 2272	. 2
3		elun 3314	. 2 $\/$
4		pnfex 8126	. . . . 5
5		mnfxr 8129	. . . . . 6
6	5	elexi 2784	. . . . 5
7	4, 6	elpr2 3655	. . . 4 $\/$
8	7	orbi2i 764	. . 3 $\/$ $\/$ $\/$
9		3orass 984	. . 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 710 $\/$ w3o 980

wceq 1373

wcel 2176

cun 3164

cpr 3634

cr 7924

cpnf 8104

cmnf 8105

cxr 8106

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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-sep 4162 ax-pow 4218 ax-un 4480 ax-cnex 8016

This theorem depends on definitions: df-bi 117 df-3or 982 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-rex 2490 df-v 2774 df-un 3170 df-in 3172 df-ss 3179 df-pw 3618 df-sn 3639 df-pr 3640 df-uni 3851 df-pnf 8109 df-mnf 8110 df-xr 8111

This theorem is referenced by: xrnemnf 9899 xrnepnf 9900 xrltnr 9901 xrltnsym 9915 xrlttr 9917 xrltso 9918 xrlttri3 9919 nltpnft 9936 npnflt 9937 ngtmnft 9939 nmnfgt 9940 xrrebnd 9941 xnegcl 9954 xnegneg 9955 xltnegi 9957 xrpnfdc 9964 xrmnfdc 9965 xnegid 9981 xaddcom 9983 xaddid1 9984 xnegdi 9990 xleadd1a 9995 xltadd1 9998 xlt2add 10002 xsubge0 10003 xposdif 10004 xleaddadd 10009 qbtwnxr 10400 xrmaxiflemcl 11556 xrmaxifle 11557 xrmaxiflemab 11558 xrmaxiflemlub 11559 xrmaxltsup 11569 xrmaxadd 11572 xrbdtri 11587 isxmet2d 14820 blssioo 15025