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 12261

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 10415	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2851	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3976	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 10429	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 10434	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3415	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4422	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 899	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1074	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 270	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 289	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 198 ∨ wo 836 ∨ w3o 1070 = wceq 1601 ∈ wcel 2107 ∪ cun 3790 {cpr 4400 ℝcr 10271 +∞cpnf 10408 -∞cmnf 10409 ℝ^*cxr 10410

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 ax-sep 5017 ax-pow 5077 ax-un 7226 ax-cnex 10328

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rex 3096 df-v 3400 df-un 3797 df-in 3799 df-ss 3806 df-pw 4381 df-sn 4399 df-pr 4401 df-uni 4672 df-pnf 10413 df-mnf 10414 df-xr 10415

This theorem is referenced by: xrnemnf 12262 xrnepnf 12263 xrltnr 12264 xrltnsym 12280 xrlttri 12282 xrlttr 12283 xrrebnd 12311 qbtwnxr 12343 xnegcl 12356 xnegneg 12357 xltnegi 12359 xaddf 12367 xnegid 12381 xaddcom 12383 xaddid1 12384 xnegdi 12390 xleadd1a 12395 xlt2add 12402 xsubge0 12403 xmullem 12406 xmulid1 12421 xmulgt0 12425 xmulasslem3 12428 xlemul1a 12430 xadddilem 12436 xadddi2 12439 xrsupsslem 12449 xrinfmsslem 12450 xrub 12454 reltxrnmnf 12484 isxmet2d 22540 blssioo 23006 ioombl1 23766 ismbf2d 23844 itg2seq 23946 xaddeq0 30083 iooelexlt 33805 relowlssretop 33806 iccpartiltu 42390 iccpartigtl 42391