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 13083

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 11219	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2821	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4119	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11234	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11238	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3473	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4619	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 912	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1089	. . 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 847 ∨ w3o 1085 = wceq 1540 ∈ wcel 2109 ∪ cun 3915 {cpr 4594 ℝcr 11074 +∞cpnf 11212 -∞cmnf 11213 ℝ^*cxr 11214

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2702 ax-sep 5254 ax-pow 5323 ax-un 7714 ax-cnex 11131

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-tru 1543 df-ex 1780 df-sb 2066 df-clab 2709 df-cleq 2722 df-clel 2804 df-v 3452 df-un 3922 df-ss 3934 df-pw 4568 df-sn 4593 df-pr 4595 df-uni 4875 df-pnf 11217 df-mnf 11218 df-xr 11219

This theorem is referenced by: xrnemnf 13084 xrnepnf 13085 xrltnr 13086 xrltnsym 13104 xrlttri 13106 xrlttr 13107 xrrebnd 13135 qbtwnxr 13167 xnegcl 13180 xnegneg 13181 xltnegi 13183 xaddf 13191 xnegid 13205 xaddcom 13207 xaddrid 13208 xnegdi 13215 xleadd1a 13220 xlt2add 13227 xsubge0 13228 xmullem 13231 xmulrid 13246 xmulgt0 13250 xmulasslem3 13253 xlemul1a 13255 xadddilem 13261 xadddi2 13264 xrsupsslem 13274 xrinfmsslem 13275 xrub 13279 reltxrnmnf 13310 isxmet2d 24222 blssioo 24690 ioombl1 25470 ismbf2d 25548 itg2seq 25650 xaddeq0 32683 rexmul2 32684 iooelexlt 37357 relowlssretop 37358 iccpartiltu 47427 iccpartigtl 47428