elxr - Intuitionistic Logic Explorer

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

Theorem elxr 9897

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 8110	. . 3
2	1	eleq2i 2271	. 2
3		elun 3313	. 2 $\/$
4		pnfex 8125	. . . . 5
5		mnfxr 8128	. . . . . 6
6	5	elexi 2783	. . . . 5
7	4, 6	elpr2 3654	. . . 4 $\/$
8	7	orbi2i 763	. . 3 $\/$ $\/$ $\/$
9		3orass 983	. . 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 979

wceq 1372

wcel 2175

cun 3163

cpr 3633

cr 7923

cpnf 8103

cmnf 8104

cxr 8105

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 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-sep 4161 ax-pow 4217 ax-un 4479 ax-cnex 8015

This theorem depends on definitions: df-bi 117 df-3or 981 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-rex 2489 df-v 2773 df-un 3169 df-in 3171 df-ss 3178 df-pw 3617 df-sn 3638 df-pr 3639 df-uni 3850 df-pnf 8108 df-mnf 8109 df-xr 8110

This theorem is referenced by: xrnemnf 9898 xrnepnf 9899 xrltnr 9900 xrltnsym 9914 xrlttr 9916 xrltso 9917 xrlttri3 9918 nltpnft 9935 npnflt 9936 ngtmnft 9938 nmnfgt 9939 xrrebnd 9940 xnegcl 9953 xnegneg 9954 xltnegi 9956 xrpnfdc 9963 xrmnfdc 9964 xnegid 9980 xaddcom 9982 xaddid1 9983 xnegdi 9989 xleadd1a 9994 xltadd1 9997 xlt2add 10001 xsubge0 10002 xposdif 10003 xleaddadd 10008 qbtwnxr 10398 xrmaxiflemcl 11527 xrmaxifle 11528 xrmaxiflemab 11529 xrmaxiflemlub 11530 xrmaxltsup 11540 xrmaxadd 11543 xrbdtri 11558 isxmet2d 14791 blssioo 14996