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 13067

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 11183	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2828	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4093	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11198	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11202	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3452	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4594	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 913	. . 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 848 ∨ w3o 1086 = wceq 1542 ∈ wcel 2114 ∪ cun 3887 {cpr 4569 ℝcr 11037 +∞cpnf 11176 -∞cmnf 11177 ℝ^*cxr 11178

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2708 ax-sep 5231 ax-pow 5307 ax-un 7689 ax-cnex 11094

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-tru 1545 df-ex 1782 df-sb 2069 df-clab 2715 df-cleq 2728 df-clel 2811 df-v 3431 df-un 3894 df-ss 3906 df-pw 4543 df-sn 4568 df-pr 4570 df-uni 4851 df-pnf 11181 df-mnf 11182 df-xr 11183

This theorem is referenced by: xrnemnf 13068 xrnepnf 13069 xrltnr 13070 xrltnsym 13088 xrlttri 13090 xrlttr 13091 xrrebnd 13120 qbtwnxr 13152 xnegcl 13165 xnegneg 13166 xltnegi 13168 xaddf 13176 xnegid 13190 xaddcom 13192 xaddrid 13193 xnegdi 13200 xleadd1a 13205 xlt2add 13212 xsubge0 13213 xmullem 13216 xmulrid 13231 xmulgt0 13235 xmulasslem3 13238 xlemul1a 13240 xadddilem 13246 xadddi2 13249 xrsupsslem 13259 xrinfmsslem 13260 xrub 13264 reltxrnmnf 13295 isxmet2d 24292 blssioo 24760 ioombl1 25529 ismbf2d 25607 itg2seq 25709 xaddeq0 32826 rexmul2 32827 iooelexlt 37678 relowlssretop 37679 iccpartiltu 47882 iccpartigtl 47883