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 13030

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 11170	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2828	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4105	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11185	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11189	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3463	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4607	. . . 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 3899 {cpr 4582 ℝcr 11025 +∞cpnf 11163 -∞cmnf 11164 ℝ^*cxr 11165

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 2708 ax-sep 5241 ax-pow 5310 ax-un 7680 ax-cnex 11082

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 2715 df-cleq 2728 df-clel 2811 df-v 3442 df-un 3906 df-ss 3918 df-pw 4556 df-sn 4581 df-pr 4583 df-uni 4864 df-pnf 11168 df-mnf 11169 df-xr 11170

This theorem is referenced by: xrnemnf 13031 xrnepnf 13032 xrltnr 13033 xrltnsym 13051 xrlttri 13053 xrlttr 13054 xrrebnd 13083 qbtwnxr 13115 xnegcl 13128 xnegneg 13129 xltnegi 13131 xaddf 13139 xnegid 13153 xaddcom 13155 xaddrid 13156 xnegdi 13163 xleadd1a 13168 xlt2add 13175 xsubge0 13176 xmullem 13179 xmulrid 13194 xmulgt0 13198 xmulasslem3 13201 xlemul1a 13203 xadddilem 13209 xadddi2 13212 xrsupsslem 13222 xrinfmsslem 13223 xrub 13227 reltxrnmnf 13258 isxmet2d 24271 blssioo 24739 ioombl1 25519 ismbf2d 25597 itg2seq 25699 xaddeq0 32833 rexmul2 32834 iooelexlt 37563 relowlssretop 37564 iccpartiltu 47664 iccpartigtl 47665