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 13012

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 11147	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2823	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4103	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11162	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11166	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3459	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4603	. . . 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 2111 ∪ cun 3900 {cpr 4578 ℝcr 11002 +∞cpnf 11140 -∞cmnf 11141 ℝ^*cxr 11142

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 2113 ax-9 2121 ax-ext 2703 ax-sep 5234 ax-pow 5303 ax-un 7668 ax-cnex 11059

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 2710 df-cleq 2723 df-clel 2806 df-v 3438 df-un 3907 df-ss 3919 df-pw 4552 df-sn 4577 df-pr 4579 df-uni 4860 df-pnf 11145 df-mnf 11146 df-xr 11147

This theorem is referenced by: xrnemnf 13013 xrnepnf 13014 xrltnr 13015 xrltnsym 13033 xrlttri 13035 xrlttr 13036 xrrebnd 13064 qbtwnxr 13096 xnegcl 13109 xnegneg 13110 xltnegi 13112 xaddf 13120 xnegid 13134 xaddcom 13136 xaddrid 13137 xnegdi 13144 xleadd1a 13149 xlt2add 13156 xsubge0 13157 xmullem 13160 xmulrid 13175 xmulgt0 13179 xmulasslem3 13182 xlemul1a 13184 xadddilem 13190 xadddi2 13193 xrsupsslem 13203 xrinfmsslem 13204 xrub 13208 reltxrnmnf 13239 isxmet2d 24240 blssioo 24708 ioombl1 25488 ismbf2d 25566 itg2seq 25668 xaddeq0 32731 rexmul2 32732 iooelexlt 37395 relowlssretop 37396 iccpartiltu 47452 iccpartigtl 47453