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 13036

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 11172	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2820	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4106	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11187	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11191	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3461	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4606	. . . 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 1540 ∈ wcel 2109 ∪ cun 3903 {cpr 4581 ℝcr 11027 +∞cpnf 11165 -∞cmnf 11166 ℝ^*cxr 11167

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 ax-sep 5238 ax-pow 5307 ax-un 7675 ax-cnex 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-tru 1543 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-v 3440 df-un 3910 df-ss 3922 df-pw 4555 df-sn 4580 df-pr 4582 df-uni 4862 df-pnf 11170 df-mnf 11171 df-xr 11172

This theorem is referenced by: xrnemnf 13037 xrnepnf 13038 xrltnr 13039 xrltnsym 13057 xrlttri 13059 xrlttr 13060 xrrebnd 13088 qbtwnxr 13120 xnegcl 13133 xnegneg 13134 xltnegi 13136 xaddf 13144 xnegid 13158 xaddcom 13160 xaddrid 13161 xnegdi 13168 xleadd1a 13173 xlt2add 13180 xsubge0 13181 xmullem 13184 xmulrid 13199 xmulgt0 13203 xmulasslem3 13206 xlemul1a 13208 xadddilem 13214 xadddi2 13217 xrsupsslem 13227 xrinfmsslem 13228 xrub 13232 reltxrnmnf 13263 isxmet2d 24231 blssioo 24699 ioombl1 25479 ismbf2d 25557 itg2seq 25659 xaddeq0 32709 rexmul2 32710 iooelexlt 37335 relowlssretop 37336 iccpartiltu 47407 iccpartigtl 47408