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 13159

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 11300	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2832	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4152	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11315	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11319	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3502	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4651	. . . 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 1539 ∈ wcel 2107 ∪ cun 3948 {cpr 4627 ℝcr 11155 +∞cpnf 11293 -∞cmnf 11294 ℝ^*cxr 11295

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 ax-sep 5295 ax-pow 5364 ax-un 7756 ax-cnex 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-un 3955 df-ss 3967 df-pw 4601 df-sn 4626 df-pr 4628 df-uni 4907 df-pnf 11298 df-mnf 11299 df-xr 11300

This theorem is referenced by: xrnemnf 13160 xrnepnf 13161 xrltnr 13162 xrltnsym 13180 xrlttri 13182 xrlttr 13183 xrrebnd 13211 qbtwnxr 13243 xnegcl 13256 xnegneg 13257 xltnegi 13259 xaddf 13267 xnegid 13281 xaddcom 13283 xaddrid 13284 xnegdi 13291 xleadd1a 13296 xlt2add 13303 xsubge0 13304 xmullem 13307 xmulrid 13322 xmulgt0 13326 xmulasslem3 13329 xlemul1a 13331 xadddilem 13337 xadddi2 13340 xrsupsslem 13350 xrinfmsslem 13351 xrub 13355 reltxrnmnf 13385 isxmet2d 24338 blssioo 24817 ioombl1 25598 ismbf2d 25676 itg2seq 25778 xaddeq0 32758 iooelexlt 37364 relowlssretop 37365 iccpartiltu 47414 iccpartigtl 47415