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 13272

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 11374	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2856	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4155	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11389	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11393	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3476	. . . . 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 2147 ∪ cun 4152 {cpr 4590 ℝcr 11226 +∞cpnf 11367 -∞cmnf 11368 ℝ^*cxr 11369

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-ext 2735 ax-sep 5252 ax-pow 5331 ax-un 7775 ax-cnex 11283

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 2102 df-clab 2742 df-cleq 2755 df-clel 2839 df-v 3456 df-ss 3901 df-un 4154 df-pw 4562 df-sn 4589 df-pr 4591 df-uni 4871 df-pnf 11372 df-mnf 11373 df-xr 11374

This theorem is used by: xrnemnf 13273 xrnepnf 13274 xrltnr 13275 xrltnsym 13293 xrlttri 13295 xrlttr 13296 xrrebnd 13325 qbtwnxr 13357 xnegcl 13370 xnegneg 13371 xltnegi 13373 xaddf 13381 xnegid 13395 xaddcom 13397 xaddrid 13398 xnegdi 13405 xleadd1a 13410 xlt2add 13417 xsubge0 13418 xmullem 13421 xmulrid 13436 xmulgt0 13440 xmulasslem3 13443 xlemul1a 13445 xadddilem 13451 xadddi2 13454 xrsupsslem 13464 xrinfmsslem 13465 xrub 13469 reltxrnmnf 13500 isxmet2d 24676 blssioo 25144 ioombl1 25913 ismbf2d 25991 itg2seq 26093 xaddeq0 33415 rexmul2 33416 iooelexlt 38477 relowlssretop 38478 iccpartiltu 48709 iccpartigtl 48710

W3C validator