mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 8211

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 8192	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8208	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4267	. . . . 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 8193	. 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 8006 +∞cpnf 8186 -∞cmnf 8187 ℝ^*cxr 8188

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 4258 ax-un 4524 ax-cnex 8098

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 8191 df-mnf 8192 df-xr 8193

This theorem is referenced by: elxr 9980 xrltnr 9983 mnflt 9987 mnfltpnf 9989 nltmnf 9992 mnfle 9996 xrltnsym 9997 xrlttri3 10001 ngtmnft 10021 xrrebnd 10023 xrre2 10025 xrre3 10026 ge0gtmnf 10027 xnegcl 10036 xltnegi 10039 xaddf 10048 xaddval 10049 xaddmnf1 10052 xaddmnf2 10053 pnfaddmnf 10054 mnfaddpnf 10055 xrex 10060 xltadd1 10080 xlt2add 10084 xsubge0 10085 xposdif 10086 xleaddadd 10091 elioc2 10140 elico2 10141 elicc2 10142 ioomax 10152 iccmax 10153 elioomnf 10172 unirnioo 10177 xrmaxadd 11780 reopnap 15228 blssioo 15235 tgioo 15236

W3C validator