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 13179

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 11328	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2836	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4176	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11343	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11347	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3511	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4674	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 911	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1090	. . 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 846 ∨ w3o 1086 = wceq 1537 ∈ wcel 2108 ∪ cun 3974 {cpr 4650 ℝcr 11183 +∞cpnf 11321 -∞cmnf 11322 ℝ^*cxr 11323

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 ax-sep 5317 ax-pow 5383 ax-un 7770 ax-cnex 11240

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-tru 1540 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-v 3490 df-un 3981 df-ss 3993 df-pw 4624 df-sn 4649 df-pr 4651 df-uni 4932 df-pnf 11326 df-mnf 11327 df-xr 11328

This theorem is referenced by: xrnemnf 13180 xrnepnf 13181 xrltnr 13182 xrltnsym 13199 xrlttri 13201 xrlttr 13202 xrrebnd 13230 qbtwnxr 13262 xnegcl 13275 xnegneg 13276 xltnegi 13278 xaddf 13286 xnegid 13300 xaddcom 13302 xaddrid 13303 xnegdi 13310 xleadd1a 13315 xlt2add 13322 xsubge0 13323 xmullem 13326 xmulrid 13341 xmulgt0 13345 xmulasslem3 13348 xlemul1a 13350 xadddilem 13356 xadddi2 13359 xrsupsslem 13369 xrinfmsslem 13370 xrub 13374 reltxrnmnf 13404 isxmet2d 24358 blssioo 24836 ioombl1 25616 ismbf2d 25694 itg2seq 25797 xaddeq0 32760 iooelexlt 37328 relowlssretop 37329 iccpartiltu 47296 iccpartigtl 47297