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 13226

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 11328	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2853	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4100	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11343	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11347	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3473	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4611	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 926	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1106	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 281	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 300	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∨ wo 861 ∨ w3o 1102 = wceq 1570 ∈ wcel 2145 ∪ cun 3897 {cpr 4586 ℝcr 11180 +∞cpnf 11321 -∞cmnf 11322 ℝ^*cxr 11323

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2733 ax-sep 5249 ax-pow 5327 ax-un 7740 ax-cnex 11237

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2740 df-cleq 2753 df-clel 2836 df-v 3453 df-un 3904 df-ss 3916 df-pw 4559 df-sn 4585 df-pr 4587 df-uni 4868 df-pnf 11326 df-mnf 11327 df-xr 11328

This theorem is used by: xrnemnf 13227 xrnepnf 13228 xrltnr 13229 xrltnsym 13247 xrlttri 13249 xrlttr 13250 xrrebnd 13279 qbtwnxr 13311 xnegcl 13324 xnegneg 13325 xltnegi 13327 xaddf 13335 xnegid 13349 xaddcom 13351 xaddrid 13352 xnegdi 13359 xleadd1a 13364 xlt2add 13371 xsubge0 13372 xmullem 13375 xmulrid 13390 xmulgt0 13394 xmulasslem3 13397 xlemul1a 13399 xadddilem 13405 xadddi2 13408 xrsupsslem 13418 xrinfmsslem 13419 xrub 13423 reltxrnmnf 13454 isxmet2d 24626 blssioo 25094 ioombl1 25863 ismbf2d 25941 itg2seq 26043 xaddeq0 33327 rexmul2 33328 iooelexlt 38253 relowlssretop 38254 iccpartiltu 48448 iccpartigtl 48449

W3C validator