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 13142

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 11248	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2855	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4108	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11263	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11267	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3477	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4617	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 925	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1106	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 281	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 300	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 209 ∨ wo 860 ∨ w3o 1102 = wceq 1570 ∈ wcel 2143 ∪ cun 3904 {cpr 4592 ℝcr 11100 +∞cpnf 11241 -∞cmnf 11242 ℝ^*cxr 11243

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-ext 2735 ax-sep 5258 ax-pow 5338 ax-un 7734 ax-cnex 11157

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-tru 1573 df-ex 1810 df-sb 2097 df-clab 2742 df-cleq 2755 df-clel 2838 df-v 3457 df-un 3911 df-ss 3923 df-pw 4565 df-sn 4591 df-pr 4593 df-uni 4874 df-pnf 11246 df-mnf 11247 df-xr 11248

This theorem is referenced by: xrnemnf 13143 xrnepnf 13144 xrltnr 13145 xrltnsym 13163 xrlttri 13165 xrlttr 13166 xrrebnd 13195 qbtwnxr 13227 xnegcl 13240 xnegneg 13241 xltnegi 13243 xaddf 13251 xnegid 13265 xaddcom 13267 xaddrid 13268 xnegdi 13275 xleadd1a 13280 xlt2add 13287 xsubge0 13288 xmullem 13291 xmulrid 13306 xmulgt0 13310 xmulasslem3 13313 xlemul1a 13315 xadddilem 13321 xadddi2 13324 xrsupsslem 13334 xrinfmsslem 13335 xrub 13339 reltxrnmnf 13370 isxmet2d 24465 blssioo 24933 ioombl1 25702 ismbf2d 25780 itg2seq 25882 xaddeq0 33076 rexmul2 33077 iooelexlt 37986 relowlssretop 37987 iccpartiltu 48148 iccpartigtl 48149