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 11950

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 10078	. . 3 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2693	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3753	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 10093	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 10096	. . . . . 6 ⊢ -∞ ∈ ℝ^*
6	5	elexi 3213	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4199	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 541	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1040	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 267	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 286	1 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 196 ∨ wo 383 ∨ w3o 1036 = wceq 1483 ∈ wcel 1990 ∪ cun 3572 {cpr 4179 ℝcr 9935 +∞cpnf 10071 -∞cmnf 10072 ℝ^*cxr 10073

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-pow 4843 ax-un 6949 ax-cnex 9992

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-v 3202 df-un 3579 df-in 3581 df-ss 3588 df-pw 4160 df-sn 4178 df-pr 4180 df-uni 4437 df-pnf 10076 df-mnf 10077 df-xr 10078

This theorem is referenced by: xrnemnf 11951 xrnepnf 11952 xrltnr 11953 xrltnsym 11970 xrlttri 11972 xrlttr 11973 xrrebnd 11999 qbtwnxr 12031 xnegcl 12044 xnegneg 12045 xltnegi 12047 xaddf 12055 xnegid 12069 xaddcom 12071 xaddid1 12072 xnegdi 12078 xleadd1a 12083 xlt2add 12090 xsubge0 12091 xmullem 12094 xmulid1 12109 xmulgt0 12113 xmulasslem3 12116 xlemul1a 12118 xadddilem 12124 xadddi2 12127 xrsupsslem 12137 xrinfmsslem 12138 xrub 12142 reltxrnmnf 12172 isxmet2d 22132 blssioo 22598 ioombl1 23330 ismbf2d 23408 itg2seq 23509 xaddeq0 29518 iooelexlt 33210 relowlssretop 33211 iccpartiltu 41358 iccpartigtl 41359