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 13065

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 11181	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2832	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4090	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11196	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11200	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3455	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4589	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 918	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1095	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 279	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 298	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 207 ∨ wo 853 ∨ w3o 1091 = wceq 1547 ∈ wcel 2119 ∪ cun 3888 {cpr 4564 ℝcr 11035 +∞cpnf 11174 -∞cmnf 11175 ℝ^*cxr 11176

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-ext 2712 ax-sep 5225 ax-pow 5301 ax-un 7685 ax-cnex 11092

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-tru 1550 df-ex 1787 df-sb 2074 df-clab 2719 df-cleq 2732 df-clel 2815 df-v 3434 df-un 3895 df-ss 3907 df-pw 4538 df-sn 4563 df-pr 4565 df-uni 4846 df-pnf 11179 df-mnf 11180 df-xr 11181

This theorem is referenced by: xrnemnf 13066 xrnepnf 13067 xrltnr 13068 xrltnsym 13086 xrlttri 13088 xrlttr 13089 xrrebnd 13118 qbtwnxr 13150 xnegcl 13163 xnegneg 13164 xltnegi 13166 xaddf 13174 xnegid 13188 xaddcom 13190 xaddrid 13191 xnegdi 13198 xleadd1a 13203 xlt2add 13210 xsubge0 13211 xmullem 13214 xmulrid 13229 xmulgt0 13233 xmulasslem3 13236 xlemul1a 13238 xadddilem 13244 xadddi2 13247 xrsupsslem 13257 xrinfmsslem 13258 xrub 13262 reltxrnmnf 13293 isxmet2d 24317 blssioo 24785 ioombl1 25554 ismbf2d 25632 itg2seq 25734 xaddeq0 32852 rexmul2 32853 iooelexlt 37731 relowlssretop 37732 iccpartiltu 47904 iccpartigtl 47905