mnfxr - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mnfxr		GIF version

Theorem mnfxr 8219

Description: Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)

**Assertion**
Ref	Expression
mnfxr	⊢ -∞ ∈ ℝ^*

**Proof of Theorem mnfxr**
Step	Hyp	Ref	Expression
1		df-mnf 8200	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8216	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4268	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2302	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3773	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3372	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8201	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2305	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2200 Vcvv 2799 ∪ cun 3195 𝒫 cpw 3649 {cpr 3667 ℝcr 8014 +∞cpnf 8194 -∞cmnf 8195 ℝ^*cxr 8196

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4202 ax-pow 4259 ax-un 4525 ax-cnex 8106

This theorem depends on definitions: df-bi 117 df-tru 1398 df-nf 1507 df-sb 1809 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-rex 2514 df-v 2801 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-uni 3889 df-pnf 8199 df-mnf 8200 df-xr 8201

This theorem is referenced by: elxr 9989 xrltnr 9992 mnflt 9996 mnfltpnf 9998 nltmnf 10001 mnfle 10005 xrltnsym 10006 xrlttri3 10010 ngtmnft 10030 xrrebnd 10032 xrre2 10034 xrre3 10035 ge0gtmnf 10036 xnegcl 10045 xltnegi 10048 xaddf 10057 xaddval 10058 xaddmnf1 10061 xaddmnf2 10062 pnfaddmnf 10063 mnfaddpnf 10064 xrex 10069 xltadd1 10089 xlt2add 10093 xsubge0 10094 xposdif 10095 xleaddadd 10100 elioc2 10149 elico2 10150 elicc2 10151 ioomax 10161 iccmax 10162 elioomnf 10181 unirnioo 10186 xrmaxadd 11793 reopnap 15241 blssioo 15248 tgioo 15249

W3C validator