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 13159

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 11265	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2858	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4110	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11280	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11284	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3480	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4621	. . . 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 2146 ∪ cun 3906 {cpr 4596 ℝcr 11117 +∞cpnf 11258 -∞cmnf 11259 ℝ^*cxr 11260

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 2148 ax-9 2156 ax-ext 2738 ax-sep 5262 ax-pow 5341 ax-un 7745 ax-cnex 11174

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 2745 df-cleq 2758 df-clel 2841 df-v 3460 df-un 3913 df-ss 3925 df-pw 4569 df-sn 4595 df-pr 4597 df-uni 4878 df-pnf 11263 df-mnf 11264 df-xr 11265

This theorem is used by: xrnemnf 13160 xrnepnf 13161 xrltnr 13162 xrltnsym 13180 xrlttri 13182 xrlttr 13183 xrrebnd 13212 qbtwnxr 13244 xnegcl 13257 xnegneg 13258 xltnegi 13260 xaddf 13268 xnegid 13282 xaddcom 13284 xaddrid 13285 xnegdi 13292 xleadd1a 13297 xlt2add 13304 xsubge0 13305 xmullem 13308 xmulrid 13323 xmulgt0 13327 xmulasslem3 13330 xlemul1a 13332 xadddilem 13338 xadddi2 13341 xrsupsslem 13351 xrinfmsslem 13352 xrub 13356 reltxrnmnf 13387 isxmet2d 24521 blssioo 24989 ioombl1 25758 ismbf2d 25836 itg2seq 25938 xaddeq0 33135 rexmul2 33136 iooelexlt 38049 relowlssretop 38050 iccpartiltu 48212 iccpartigtl 48213

W3C validator