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 13056

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 2829	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4094	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11187	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11191	. . . . . 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 11026 +∞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 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 5300 ax-un 7680 ax-cnex 11083

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 11170 df-mnf 11171 df-xr 11172

This theorem is referenced by: xrnemnf 13057 xrnepnf 13058 xrltnr 13059 xrltnsym 13077 xrlttri 13079 xrlttr 13080 xrrebnd 13109 qbtwnxr 13141 xnegcl 13154 xnegneg 13155 xltnegi 13157 xaddf 13165 xnegid 13179 xaddcom 13181 xaddrid 13182 xnegdi 13189 xleadd1a 13194 xlt2add 13201 xsubge0 13202 xmullem 13205 xmulrid 13220 xmulgt0 13224 xmulasslem3 13227 xlemul1a 13229 xadddilem 13235 xadddi2 13238 xrsupsslem 13248 xrinfmsslem 13249 xrub 13253 reltxrnmnf 13284 isxmet2d 24301 blssioo 24769 ioombl1 25538 ismbf2d 25616 itg2seq 25718 xaddeq0 32846 rexmul2 32847 iooelexlt 37689 relowlssretop 37690 iccpartiltu 47879 iccpartigtl 47880