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 11826

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 9957	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2680	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3715	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 9972	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 9975	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3186	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4147	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 540	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1034	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 266	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 285	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 195 ∨ wo 382 ∨ w3o 1030 = wceq 1475 ∈ wcel 1977 ∪ cun 3538 {cpr 4127 ℝcr 9814 +∞cpnf 9950 -∞cmnf 9951 ℝ^*cxr 9952

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-pow 4769 ax-un 6847 ax-cnex 9871

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-v 3175 df-un 3545 df-in 3547 df-ss 3554 df-pw 4110 df-sn 4126 df-pr 4128 df-uni 4373 df-pnf 9955 df-mnf 9956 df-xr 9957

This theorem is referenced by: xrnemnf 11827 xrnepnf 11828 xrltnr 11829 xrltnsym 11846 xrlttri 11848 xrlttr 11849 xrrebnd 11873 qbtwnxr 11905 xnegcl 11918 xnegneg 11919 xltnegi 11921 xaddf 11929 xnegid 11943 xaddcom 11945 xaddid1 11946 xnegdi 11950 xleadd1a 11955 xlt2add 11962 xsubge0 11963 xmullem 11966 xmulid1 11981 xmulgt0 11985 xmulasslem3 11988 xlemul1a 11990 xadddilem 11996 xadddi2 11999 xrsupsslem 12009 xrinfmsslem 12010 xrub 12014 reltxrnmnf 12043 isxmet2d 21942 blssioo 22406 ioombl1 23137 ismbf2d 23214 itg2seq 23315 xaddeq0 28907 iooelexlt 32386 relowlssretop 32387 iccpartiltu 39960 iccpartigtl 39961