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 13248

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 11350	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2852	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4152	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11365	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11369	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3472	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4607	. . . 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 1569 ∈ wcel 2144 ∪ cun 4149 {cpr 4586 ℝcr 11202 +∞cpnf 11343 -∞cmnf 11344 ℝ^*cxr 11345

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732 ax-sep 5248 ax-pow 5326 ax-un 7751 ax-cnex 11259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-tru 1572 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-v 3452 df-ss 3896 df-un 4151 df-pw 4558 df-sn 4585 df-pr 4587 df-uni 4867 df-pnf 11348 df-mnf 11349 df-xr 11350

This theorem is used by: xrnemnf 13249 xrnepnf 13250 xrltnr 13251 xrltnsym 13269 xrlttri 13271 xrlttr 13272 xrrebnd 13301 qbtwnxr 13333 xnegcl 13346 xnegneg 13347 xltnegi 13349 xaddf 13357 xnegid 13371 xaddcom 13373 xaddrid 13374 xnegdi 13381 xleadd1a 13386 xlt2add 13393 xsubge0 13394 xmullem 13397 xmulrid 13412 xmulgt0 13416 xmulasslem3 13419 xlemul1a 13421 xadddilem 13427 xadddi2 13430 xrsupsslem 13440 xrinfmsslem 13441 xrub 13445 reltxrnmnf 13476 isxmet2d 24651 blssioo 25119 ioombl1 25888 ismbf2d 25966 itg2seq 26068 xaddeq0 33391 rexmul2 33392 iooelexlt 38378 relowlssretop 38379 iccpartiltu 48597 iccpartigtl 48598

W3C validator