elxr - Intuitionistic Logic Explorer

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

Theorem elxr 9563

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 7804	. . 3
2	1	eleq2i 2206	. 2
3		elun 3217	. 2 $\/$
4		pnfex 7819	. . . . 5
5		mnfxr 7822	. . . . . 6
6	5	elexi 2698	. . . . 5
7	4, 6	elpr2 3549	. . . 4 $\/$
8	7	orbi2i 751	. . 3 $\/$ $\/$ $\/$
9		3orass 965	. . 3 $\/$ $\/$ $\/$ $\/$
10	8, 9	bitr4i 186	. 2 $\/$ $\/$ $\/$
11	2, 3, 10	3bitri 205	1 $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wb 104 $\/$ wo 697 $\/$ w3o 961

wceq 1331

wcel 1480

cun 3069

cpr 3528

cr 7619

cpnf 7797

cmnf 7798

cxr 7799

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-un 4355 ax-cnex 7711

This theorem depends on definitions: df-bi 116 df-3or 963 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rex 2422 df-v 2688 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-uni 3737 df-pnf 7802 df-mnf 7803 df-xr 7804

This theorem is referenced by: xrnemnf 9564 xrnepnf 9565 xrltnr 9566 xrltnsym 9579 xrlttr 9581 xrltso 9582 xrlttri3 9583 nltpnft 9597 npnflt 9598 ngtmnft 9600 nmnfgt 9601 xrrebnd 9602 xnegcl 9615 xnegneg 9616 xltnegi 9618 xrpnfdc 9625 xrmnfdc 9626 xnegid 9642 xaddcom 9644 xaddid1 9645 xnegdi 9651 xleadd1a 9656 xltadd1 9659 xlt2add 9663 xsubge0 9664 xposdif 9665 xleaddadd 9670 qbtwnxr 10035 xrmaxiflemcl 11014 xrmaxifle 11015 xrmaxiflemab 11016 xrmaxiflemlub 11017 xrmaxltsup 11027 xrmaxadd 11030 xrbdtri 11045 isxmet2d 12517 blssioo 12714