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 13137

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 11278	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2827	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4133	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11293	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11297	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3487	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4633	. . . 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 3929 {cpr 4608 ℝcr 11133 +∞cpnf 11271 -∞cmnf 11272 ℝ^*cxr 11273

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 2708 ax-sep 5271 ax-pow 5340 ax-un 7734 ax-cnex 11190

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 2715 df-cleq 2728 df-clel 2810 df-v 3466 df-un 3936 df-ss 3948 df-pw 4582 df-sn 4607 df-pr 4609 df-uni 4889 df-pnf 11276 df-mnf 11277 df-xr 11278

This theorem is referenced by: xrnemnf 13138 xrnepnf 13139 xrltnr 13140 xrltnsym 13158 xrlttri 13160 xrlttr 13161 xrrebnd 13189 qbtwnxr 13221 xnegcl 13234 xnegneg 13235 xltnegi 13237 xaddf 13245 xnegid 13259 xaddcom 13261 xaddrid 13262 xnegdi 13269 xleadd1a 13274 xlt2add 13281 xsubge0 13282 xmullem 13285 xmulrid 13300 xmulgt0 13304 xmulasslem3 13307 xlemul1a 13309 xadddilem 13315 xadddi2 13318 xrsupsslem 13328 xrinfmsslem 13329 xrub 13333 reltxrnmnf 13364 isxmet2d 24271 blssioo 24739 ioombl1 25520 ismbf2d 25598 itg2seq 25700 xaddeq0 32735 rexmul2 32736 iooelexlt 37385 relowlssretop 37386 iccpartiltu 47403 iccpartigtl 47404