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 13131

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 11284	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2817	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4145	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11299	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11303	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3482	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4656	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 910	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1087	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 277	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 296	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∨ wo 845 ∨ w3o 1083 = wceq 1533 ∈ wcel 2098 ∪ cun 3942 {cpr 4632 ℝcr 11139 +∞cpnf 11277 -∞cmnf 11278 ℝ^*cxr 11279

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-pow 5365 ax-un 7741 ax-cnex 11196

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-un 3949 df-ss 3961 df-pw 4606 df-sn 4631 df-pr 4633 df-uni 4910 df-pnf 11282 df-mnf 11283 df-xr 11284

This theorem is referenced by: xrnemnf 13132 xrnepnf 13133 xrltnr 13134 xrltnsym 13151 xrlttri 13153 xrlttr 13154 xrrebnd 13182 qbtwnxr 13214 xnegcl 13227 xnegneg 13228 xltnegi 13230 xaddf 13238 xnegid 13252 xaddcom 13254 xaddrid 13255 xnegdi 13262 xleadd1a 13267 xlt2add 13274 xsubge0 13275 xmullem 13278 xmulrid 13293 xmulgt0 13297 xmulasslem3 13300 xlemul1a 13302 xadddilem 13308 xadddi2 13311 xrsupsslem 13321 xrinfmsslem 13322 xrub 13326 reltxrnmnf 13356 isxmet2d 24277 blssioo 24755 ioombl1 25535 ismbf2d 25613 itg2seq 25716 xaddeq0 32605 iooelexlt 36972 relowlssretop 36973 iccpartiltu 46899 iccpartigtl 46900