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 13058

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 11174	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2829	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4094	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11189	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11193	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3453	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4595	. . . 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 3888 {cpr 4570 ℝcr 11028 +∞cpnf 11167 -∞cmnf 11168 ℝ^*cxr 11169

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 2709 ax-sep 5231 ax-pow 5302 ax-un 7682 ax-cnex 11085

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 2716 df-cleq 2729 df-clel 2812 df-v 3432 df-un 3895 df-ss 3907 df-pw 4544 df-sn 4569 df-pr 4571 df-uni 4852 df-pnf 11172 df-mnf 11173 df-xr 11174

This theorem is referenced by: xrnemnf 13059 xrnepnf 13060 xrltnr 13061 xrltnsym 13079 xrlttri 13081 xrlttr 13082 xrrebnd 13111 qbtwnxr 13143 xnegcl 13156 xnegneg 13157 xltnegi 13159 xaddf 13167 xnegid 13181 xaddcom 13183 xaddrid 13184 xnegdi 13191 xleadd1a 13196 xlt2add 13203 xsubge0 13204 xmullem 13207 xmulrid 13222 xmulgt0 13226 xmulasslem3 13229 xlemul1a 13231 xadddilem 13237 xadddi2 13240 xrsupsslem 13250 xrinfmsslem 13251 xrub 13255 reltxrnmnf 13286 isxmet2d 24302 blssioo 24770 ioombl1 25539 ismbf2d 25617 itg2seq 25719 xaddeq0 32841 rexmul2 32842 iooelexlt 37692 relowlssretop 37693 iccpartiltu 47894 iccpartigtl 47895