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 13017

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 11157	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2825	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4102	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11172	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11176	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3460	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4602	. . . 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 1541 ∈ wcel 2113 ∪ cun 3896 {cpr 4577 ℝcr 11012 +∞cpnf 11150 -∞cmnf 11151 ℝ^*cxr 11152

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2705 ax-sep 5236 ax-pow 5305 ax-un 7674 ax-cnex 11069

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-tru 1544 df-ex 1781 df-sb 2068 df-clab 2712 df-cleq 2725 df-clel 2808 df-v 3439 df-un 3903 df-ss 3915 df-pw 4551 df-sn 4576 df-pr 4578 df-uni 4859 df-pnf 11155 df-mnf 11156 df-xr 11157

This theorem is referenced by: xrnemnf 13018 xrnepnf 13019 xrltnr 13020 xrltnsym 13038 xrlttri 13040 xrlttr 13041 xrrebnd 13069 qbtwnxr 13101 xnegcl 13114 xnegneg 13115 xltnegi 13117 xaddf 13125 xnegid 13139 xaddcom 13141 xaddrid 13142 xnegdi 13149 xleadd1a 13154 xlt2add 13161 xsubge0 13162 xmullem 13165 xmulrid 13180 xmulgt0 13184 xmulasslem3 13187 xlemul1a 13189 xadddilem 13195 xadddi2 13198 xrsupsslem 13208 xrinfmsslem 13209 xrub 13213 reltxrnmnf 13244 isxmet2d 24243 blssioo 24711 ioombl1 25491 ismbf2d 25569 itg2seq 25671 xaddeq0 32740 rexmul2 32741 iooelexlt 37427 relowlssretop 37428 iccpartiltu 47546 iccpartigtl 47547