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 13076

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 11212	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2820	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4116	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11227	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11231	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3470	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4616	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 912	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1089	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 278	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 297	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∨ wo 847 ∨ w3o 1085 = wceq 1540 ∈ wcel 2109 ∪ cun 3912 {cpr 4591 ℝcr 11067 +∞cpnf 11205 -∞cmnf 11206 ℝ^*cxr 11207

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 ax-sep 5251 ax-pow 5320 ax-un 7711 ax-cnex 11124

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-tru 1543 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-v 3449 df-un 3919 df-ss 3931 df-pw 4565 df-sn 4590 df-pr 4592 df-uni 4872 df-pnf 11210 df-mnf 11211 df-xr 11212

This theorem is referenced by: xrnemnf 13077 xrnepnf 13078 xrltnr 13079 xrltnsym 13097 xrlttri 13099 xrlttr 13100 xrrebnd 13128 qbtwnxr 13160 xnegcl 13173 xnegneg 13174 xltnegi 13176 xaddf 13184 xnegid 13198 xaddcom 13200 xaddrid 13201 xnegdi 13208 xleadd1a 13213 xlt2add 13220 xsubge0 13221 xmullem 13224 xmulrid 13239 xmulgt0 13243 xmulasslem3 13246 xlemul1a 13248 xadddilem 13254 xadddi2 13257 xrsupsslem 13267 xrinfmsslem 13268 xrub 13272 reltxrnmnf 13303 isxmet2d 24215 blssioo 24683 ioombl1 25463 ismbf2d 25541 itg2seq 25643 xaddeq0 32676 rexmul2 32677 iooelexlt 37350 relowlssretop 37351 iccpartiltu 47423 iccpartigtl 47424