elxr - Intuitionistic Logic Explorer

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

Theorem elxr 9868

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 8082	. . 3
2	1	eleq2i 2263	. 2
3		elun 3305	. 2 $\/$
4		pnfex 8097	. . . . 5
5		mnfxr 8100	. . . . . 6
6	5	elexi 2775	. . . . 5
7	4, 6	elpr2 3645	. . . 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 1364

wcel 2167

cun 3155

cpr 3624

cr 7895

cpnf 8075

cmnf 8076

cxr 8077

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-pow 4208 ax-un 4469 ax-cnex 7987

This theorem depends on definitions: df-bi 117 df-3or 981 df-tru 1367 df-nf 1475 df-sb 1777 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-rex 2481 df-v 2765 df-un 3161 df-in 3163 df-ss 3170 df-pw 3608 df-sn 3629 df-pr 3630 df-uni 3841 df-pnf 8080 df-mnf 8081 df-xr 8082

This theorem is referenced by: xrnemnf 9869 xrnepnf 9870 xrltnr 9871 xrltnsym 9885 xrlttr 9887 xrltso 9888 xrlttri3 9889 nltpnft 9906 npnflt 9907 ngtmnft 9909 nmnfgt 9910 xrrebnd 9911 xnegcl 9924 xnegneg 9925 xltnegi 9927 xrpnfdc 9934 xrmnfdc 9935 xnegid 9951 xaddcom 9953 xaddid1 9954 xnegdi 9960 xleadd1a 9965 xltadd1 9968 xlt2add 9972 xsubge0 9973 xposdif 9974 xleaddadd 9979 qbtwnxr 10364 xrmaxiflemcl 11427 xrmaxifle 11428 xrmaxiflemab 11429 xrmaxiflemlub 11430 xrmaxltsup 11440 xrmaxadd 11443 xrbdtri 11458 isxmet2d 14668 blssioo 14873