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 13042

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 11182	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2829	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4107	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11197	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11201	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3465	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4609	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 913	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1090	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 278	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 297	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∨ wo 848 ∨ w3o 1086 = wceq 1542 ∈ wcel 2114 ∪ cun 3901 {cpr 4584 ℝcr 11037 +∞cpnf 11175 -∞cmnf 11176 ℝ^*cxr 11177

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-sep 5243 ax-pow 5312 ax-un 7690 ax-cnex 11094

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-tru 1545 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-v 3444 df-un 3908 df-ss 3920 df-pw 4558 df-sn 4583 df-pr 4585 df-uni 4866 df-pnf 11180 df-mnf 11181 df-xr 11182

This theorem is referenced by: xrnemnf 13043 xrnepnf 13044 xrltnr 13045 xrltnsym 13063 xrlttri 13065 xrlttr 13066 xrrebnd 13095 qbtwnxr 13127 xnegcl 13140 xnegneg 13141 xltnegi 13143 xaddf 13151 xnegid 13165 xaddcom 13167 xaddrid 13168 xnegdi 13175 xleadd1a 13180 xlt2add 13187 xsubge0 13188 xmullem 13191 xmulrid 13206 xmulgt0 13210 xmulasslem3 13213 xlemul1a 13215 xadddilem 13221 xadddi2 13224 xrsupsslem 13234 xrinfmsslem 13235 xrub 13239 reltxrnmnf 13270 isxmet2d 24283 blssioo 24751 ioombl1 25531 ismbf2d 25609 itg2seq 25711 xaddeq0 32843 rexmul2 32844 iooelexlt 37611 relowlssretop 37612 iccpartiltu 47776 iccpartigtl 47777