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 12863

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 11024	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2832	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4088	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11039	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11043	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3450	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4592	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 910	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1089	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 277	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 297	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∨ wo 844 ∨ w3o 1085 = wceq 1542 ∈ wcel 2110 ∪ cun 3890 {cpr 4569 ℝcr 10881 +∞cpnf 11017 -∞cmnf 11018 ℝ^*cxr 11019

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 ax-sep 5227 ax-pow 5292 ax-un 7583 ax-cnex 10938

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-tru 1545 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-v 3433 df-un 3897 df-in 3899 df-ss 3909 df-pw 4541 df-sn 4568 df-pr 4570 df-uni 4846 df-pnf 11022 df-mnf 11023 df-xr 11024

This theorem is referenced by: xrnemnf 12864 xrnepnf 12865 xrltnr 12866 xrltnsym 12882 xrlttri 12884 xrlttr 12885 xrrebnd 12913 qbtwnxr 12945 xnegcl 12958 xnegneg 12959 xltnegi 12961 xaddf 12969 xnegid 12983 xaddcom 12985 xaddid1 12986 xnegdi 12993 xleadd1a 12998 xlt2add 13005 xsubge0 13006 xmullem 13009 xmulid1 13024 xmulgt0 13028 xmulasslem3 13031 xlemul1a 13033 xadddilem 13039 xadddi2 13042 xrsupsslem 13052 xrinfmsslem 13053 xrub 13057 reltxrnmnf 13087 isxmet2d 23491 blssioo 23969 ioombl1 24737 ismbf2d 24815 itg2seq 24918 xaddeq0 31085 iooelexlt 35542 relowlssretop 35543 iccpartiltu 44853 iccpartigtl 44854