elxr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elxr		Structured version Visualization version GIF version

Theorem elxr 11988

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 10116	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2722	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3786	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 10131	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 10134	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3244	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4232	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 540	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1057	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 267	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 286	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 196 ∨ wo 382 ∨ w3o 1053 = wceq 1523 ∈ wcel 2030 ∪ cun 3605 {cpr 4212 ℝcr 9973 +∞cpnf 10109 -∞cmnf 10110 ℝ^*cxr 10111

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-pow 4873 ax-un 6991 ax-cnex 10030

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rex 2947 df-v 3233 df-un 3612 df-in 3614 df-ss 3621 df-pw 4193 df-sn 4211 df-pr 4213 df-uni 4469 df-pnf 10114 df-mnf 10115 df-xr 10116

This theorem is referenced by: xrnemnf 11989 xrnepnf 11990 xrltnr 11991 xrltnsym 12008 xrlttri 12010 xrlttr 12011 xrrebnd 12037 qbtwnxr 12069 xnegcl 12082 xnegneg 12083 xltnegi 12085 xaddf 12093 xnegid 12107 xaddcom 12109 xaddid1 12110 xnegdi 12116 xleadd1a 12121 xlt2add 12128 xsubge0 12129 xmullem 12132 xmulid1 12147 xmulgt0 12151 xmulasslem3 12154 xlemul1a 12156 xadddilem 12162 xadddi2 12165 xrsupsslem 12175 xrinfmsslem 12176 xrub 12180 reltxrnmnf 12210 isxmet2d 22179 blssioo 22645 ioombl1 23376 ismbf2d 23453 itg2seq 23554 xaddeq0 29646 iooelexlt 33340 relowlssretop 33341 iccpartiltu 41683 iccpartigtl 41684