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 12160

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 10357	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2873	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3946	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 10372	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 10375	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3403	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4388	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 927	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1103	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 269	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 288	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 197 ∨ wo 865 ∨ w3o 1099 = wceq 1637 ∈ wcel 2155 ∪ cun 3761 {cpr 4366 ℝcr 10214 +∞cpnf 10350 -∞cmnf 10351 ℝ^*cxr 10352

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2067 ax-7 2103 ax-8 2157 ax-9 2164 ax-10 2184 ax-11 2200 ax-12 2213 ax-13 2419 ax-ext 2781 ax-sep 4968 ax-pow 5029 ax-un 7173 ax-cnex 10271

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-tru 1641 df-ex 1860 df-nf 1864 df-sb 2060 df-clab 2789 df-cleq 2795 df-clel 2798 df-nfc 2933 df-rex 3098 df-v 3389 df-un 3768 df-in 3770 df-ss 3777 df-pw 4347 df-sn 4365 df-pr 4367 df-uni 4624 df-pnf 10355 df-mnf 10356 df-xr 10357

This theorem is referenced by: xrnemnf 12161 xrnepnf 12162 xrltnr 12163 xrltnsym 12180 xrlttri 12182 xrlttr 12183 xrrebnd 12211 qbtwnxr 12243 xnegcl 12256 xnegneg 12257 xltnegi 12259 xaddf 12267 xnegid 12281 xaddcom 12283 xaddid1 12284 xnegdi 12290 xleadd1a 12295 xlt2add 12302 xsubge0 12303 xmullem 12306 xmulid1 12321 xmulgt0 12325 xmulasslem3 12328 xlemul1a 12330 xadddilem 12336 xadddi2 12339 xrsupsslem 12349 xrinfmsslem 12350 xrub 12354 reltxrnmnf 12384 isxmet2d 22339 blssioo 22805 ioombl1 23537 ismbf2d 23615 itg2seq 23717 xaddeq0 29839 iooelexlt 33520 relowlssretop 33521 iccpartiltu 41927 iccpartigtl 41928