elxr - Intuitionistic Logic Explorer

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

Theorem elxr 9928

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 8141	. . 3
2	1	eleq2i 2273	. 2
3		elun 3318	. 2 $\/$
4		pnfex 8156	. . . . 5
5		mnfxr 8159	. . . . . 6
6	5	elexi 2786	. . . . 5
7	4, 6	elpr2 3660	. . . 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 2177

cun 3168

cpr 3639

cr 7954

cpnf 8134

cmnf 8135

cxr 8136

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 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4173 ax-pow 4229 ax-un 4493 ax-cnex 8046

This theorem depends on definitions: df-bi 117 df-3or 982 df-tru 1376 df-nf 1485 df-sb 1787 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-rex 2491 df-v 2775 df-un 3174 df-in 3176 df-ss 3183 df-pw 3623 df-sn 3644 df-pr 3645 df-uni 3860 df-pnf 8139 df-mnf 8140 df-xr 8141

This theorem is referenced by: xrnemnf 9929 xrnepnf 9930 xrltnr 9931 xrltnsym 9945 xrlttr 9947 xrltso 9948 xrlttri3 9949 nltpnft 9966 npnflt 9967 ngtmnft 9969 nmnfgt 9970 xrrebnd 9971 xnegcl 9984 xnegneg 9985 xltnegi 9987 xrpnfdc 9994 xrmnfdc 9995 xnegid 10011 xaddcom 10013 xaddid1 10014 xnegdi 10020 xleadd1a 10025 xltadd1 10028 xlt2add 10032 xsubge0 10033 xposdif 10034 xleaddadd 10039 qbtwnxr 10432 xrmaxiflemcl 11641 xrmaxifle 11642 xrmaxiflemab 11643 xrmaxiflemlub 11644 xrmaxltsup 11654 xrmaxadd 11657 xrbdtri 11672 isxmet2d 14905 blssioo 15110