elxr - Intuitionistic Logic Explorer

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

Theorem elxr 9450

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 7722	. . 3
2	1	eleq2i 2179	. 2
3		elun 3181	. 2 $\/$
4		pnfex 7737	. . . . 5
5		mnfxr 7740	. . . . . 6
6	5	elexi 2667	. . . . 5
7	4, 6	elpr2 3513	. . . 4 $\/$
8	7	orbi2i 734	. . 3 $\/$ $\/$ $\/$
9		3orass 946	. . 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 680 $\/$ w3o 942

wceq 1312

wcel 1461

cun 3033

cpr 3492

cr 7540

cpnf 7715

cmnf 7716

cxr 7717

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-13 1472 ax-14 1473 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-sep 4004 ax-pow 4056 ax-un 4313 ax-cnex 7630

This theorem depends on definitions: df-bi 116 df-3or 944 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-rex 2394 df-v 2657 df-un 3039 df-in 3041 df-ss 3048 df-pw 3476 df-sn 3497 df-pr 3498 df-uni 3701 df-pnf 7720 df-mnf 7721 df-xr 7722

This theorem is referenced by: xrnemnf 9451 xrnepnf 9452 xrltnr 9453 xrltnsym 9466 xrlttr 9468 xrltso 9469 xrlttri3 9470 nltpnft 9484 npnflt 9485 ngtmnft 9487 nmnfgt 9488 xrrebnd 9489 xnegcl 9502 xnegneg 9503 xltnegi 9505 xrpnfdc 9512 xrmnfdc 9513 xnegid 9529 xaddcom 9531 xaddid1 9532 xnegdi 9538 xleadd1a 9543 xltadd1 9546 xlt2add 9550 xsubge0 9551 xposdif 9552 xleaddadd 9557 qbtwnxr 9922 xrmaxiflemcl 10900 xrmaxifle 10901 xrmaxiflemab 10902 xrmaxiflemlub 10903 xrmaxltsup 10913 xrmaxadd 10916 xrbdtri 10931 isxmet2d 12331 blssioo 12525