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 12781

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 10944	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2830	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4079	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 10959	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 10963	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3441	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4583	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 909	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1088	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 277	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 296	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∨ wo 843 ∨ w3o 1084 = wceq 1539 ∈ wcel 2108 ∪ cun 3881 {cpr 4560 ℝcr 10801 +∞cpnf 10937 -∞cmnf 10938 ℝ^*cxr 10939

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709 ax-sep 5218 ax-pow 5283 ax-un 7566 ax-cnex 10858

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-tru 1542 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-v 3424 df-un 3888 df-in 3890 df-ss 3900 df-pw 4532 df-sn 4559 df-pr 4561 df-uni 4837 df-pnf 10942 df-mnf 10943 df-xr 10944

This theorem is referenced by: xrnemnf 12782 xrnepnf 12783 xrltnr 12784 xrltnsym 12800 xrlttri 12802 xrlttr 12803 xrrebnd 12831 qbtwnxr 12863 xnegcl 12876 xnegneg 12877 xltnegi 12879 xaddf 12887 xnegid 12901 xaddcom 12903 xaddid1 12904 xnegdi 12911 xleadd1a 12916 xlt2add 12923 xsubge0 12924 xmullem 12927 xmulid1 12942 xmulgt0 12946 xmulasslem3 12949 xlemul1a 12951 xadddilem 12957 xadddi2 12960 xrsupsslem 12970 xrinfmsslem 12971 xrub 12975 reltxrnmnf 13005 isxmet2d 23388 blssioo 23864 ioombl1 24631 ismbf2d 24709 itg2seq 24812 xaddeq0 30978 iooelexlt 35460 relowlssretop 35461 iccpartiltu 44762 iccpartigtl 44763