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 13115

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 11217	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2853	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4106	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11232	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11236	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3475	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4608	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 923	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1100	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 280	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 299	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 ∨ wo 858 ∨ w3o 1096 = wceq 1559 ∈ wcel 2141 ∪ cun 3902 {cpr 4583 ℝcr 11069 +∞cpnf 11210 -∞cmnf 11211 ℝ^*cxr 11212

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-ext 2733 ax-sep 5245 ax-pow 5321 ax-un 7714 ax-cnex 11126

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-tru 1562 df-ex 1799 df-sb 2090 df-clab 2740 df-cleq 2753 df-clel 2836 df-v 3455 df-un 3909 df-ss 3921 df-pw 4556 df-sn 4582 df-pr 4584 df-uni 4865 df-pnf 11215 df-mnf 11216 df-xr 11217

This theorem is referenced by: xrnemnf 13116 xrnepnf 13117 xrltnr 13118 xrltnsym 13136 xrlttri 13138 xrlttr 13139 xrrebnd 13168 qbtwnxr 13200 xnegcl 13213 xnegneg 13214 xltnegi 13216 xaddf 13224 xnegid 13238 xaddcom 13240 xaddrid 13241 xnegdi 13248 xleadd1a 13253 xlt2add 13260 xsubge0 13261 xmullem 13264 xmulrid 13279 xmulgt0 13283 xmulasslem3 13286 xlemul1a 13288 xadddilem 13294 xadddi2 13297 xrsupsslem 13307 xrinfmsslem 13308 xrub 13312 reltxrnmnf 13343 isxmet2d 24367 blssioo 24835 ioombl1 25604 ismbf2d 25682 itg2seq 25784 xaddeq0 32905 rexmul2 32906 iooelexlt 37820 relowlssretop 37821 iccpartiltu 47992 iccpartigtl 47993