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 13171

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 11275	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2854	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4103	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11290	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11294	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3475	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4614	. . . 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 2145 ∪ cun 3900 {cpr 4589 ℝcr 11127 +∞cpnf 11268 -∞cmnf 11269 ℝ^*cxr 11270

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2734 ax-sep 5255 ax-pow 5334 ax-un 7740 ax-cnex 11184

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 2100 df-clab 2741 df-cleq 2754 df-clel 2837 df-v 3455 df-un 3907 df-ss 3919 df-pw 4562 df-sn 4588 df-pr 4590 df-uni 4871 df-pnf 11273 df-mnf 11274 df-xr 11275

This theorem is used by: xrnemnf 13172 xrnepnf 13173 xrltnr 13174 xrltnsym 13192 xrlttri 13194 xrlttr 13195 xrrebnd 13224 qbtwnxr 13256 xnegcl 13269 xnegneg 13270 xltnegi 13272 xaddf 13280 xnegid 13294 xaddcom 13296 xaddrid 13297 xnegdi 13304 xleadd1a 13309 xlt2add 13316 xsubge0 13317 xmullem 13320 xmulrid 13335 xmulgt0 13339 xmulasslem3 13342 xlemul1a 13344 xadddilem 13350 xadddi2 13353 xrsupsslem 13363 xrinfmsslem 13364 xrub 13368 reltxrnmnf 13399 isxmet2d 24559 blssioo 25027 ioombl1 25796 ismbf2d 25874 itg2seq 25976 xaddeq0 33232 rexmul2 33233 iooelexlt 38124 relowlssretop 38125 iccpartiltu 48330 iccpartigtl 48331

W3C validator