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 13096

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 11252	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2826	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4149	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11267	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11271	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3494	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4654	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 912	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1091	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 278	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 297	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∨ wo 846 ∨ w3o 1087 = wceq 1542 ∈ wcel 2107 ∪ cun 3947 {cpr 4631 ℝcr 11109 +∞cpnf 11245 -∞cmnf 11246 ℝ^*cxr 11247

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-pow 5364 ax-un 7725 ax-cnex 11166

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3954 df-in 3956 df-ss 3966 df-pw 4605 df-sn 4630 df-pr 4632 df-uni 4910 df-pnf 11250 df-mnf 11251 df-xr 11252

This theorem is referenced by: xrnemnf 13097 xrnepnf 13098 xrltnr 13099 xrltnsym 13116 xrlttri 13118 xrlttr 13119 xrrebnd 13147 qbtwnxr 13179 xnegcl 13192 xnegneg 13193 xltnegi 13195 xaddf 13203 xnegid 13217 xaddcom 13219 xaddrid 13220 xnegdi 13227 xleadd1a 13232 xlt2add 13239 xsubge0 13240 xmullem 13243 xmulrid 13258 xmulgt0 13262 xmulasslem3 13265 xlemul1a 13267 xadddilem 13273 xadddi2 13276 xrsupsslem 13286 xrinfmsslem 13287 xrub 13291 reltxrnmnf 13321 isxmet2d 23833 blssioo 24311 ioombl1 25079 ismbf2d 25157 itg2seq 25260 xaddeq0 31966 iooelexlt 36243 relowlssretop 36244 iccpartiltu 46090 iccpartigtl 46091