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 13156

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 11297	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2831	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4163	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11312	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11316	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3501	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4657	. . . 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 1537 ∈ wcel 2106 ∪ cun 3961 {cpr 4633 ℝcr 11152 +∞cpnf 11290 -∞cmnf 11291 ℝ^*cxr 11292

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-pow 5371 ax-un 7754 ax-cnex 11209

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-un 3968 df-ss 3980 df-pw 4607 df-sn 4632 df-pr 4634 df-uni 4913 df-pnf 11295 df-mnf 11296 df-xr 11297

This theorem is referenced by: xrnemnf 13157 xrnepnf 13158 xrltnr 13159 xrltnsym 13176 xrlttri 13178 xrlttr 13179 xrrebnd 13207 qbtwnxr 13239 xnegcl 13252 xnegneg 13253 xltnegi 13255 xaddf 13263 xnegid 13277 xaddcom 13279 xaddrid 13280 xnegdi 13287 xleadd1a 13292 xlt2add 13299 xsubge0 13300 xmullem 13303 xmulrid 13318 xmulgt0 13322 xmulasslem3 13325 xlemul1a 13327 xadddilem 13333 xadddi2 13336 xrsupsslem 13346 xrinfmsslem 13347 xrub 13351 reltxrnmnf 13381 isxmet2d 24353 blssioo 24831 ioombl1 25611 ismbf2d 25689 itg2seq 25792 xaddeq0 32764 iooelexlt 37345 relowlssretop 37346 iccpartiltu 47347 iccpartigtl 47348