mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 8083

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 8064	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8080	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4216	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2269	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3729	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3331	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8065	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2272	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2167 Vcvv 2763 ∪ cun 3155 𝒫 cpw 3605 {cpr 3623 ℝcr 7878 +∞cpnf 8058 -∞cmnf 8059 ℝ^*cxr 8060

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 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4151 ax-pow 4207 ax-un 4468 ax-cnex 7970

This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1475 df-sb 1777 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-rex 2481 df-v 2765 df-un 3161 df-in 3163 df-ss 3170 df-pw 3607 df-sn 3628 df-pr 3629 df-uni 3840 df-pnf 8063 df-mnf 8064 df-xr 8065

This theorem is referenced by: elxr 9851 xrltnr 9854 mnflt 9858 mnfltpnf 9860 nltmnf 9863 mnfle 9867 xrltnsym 9868 xrlttri3 9872 ngtmnft 9892 xrrebnd 9894 xrre2 9896 xrre3 9897 ge0gtmnf 9898 xnegcl 9907 xltnegi 9910 xaddf 9919 xaddval 9920 xaddmnf1 9923 xaddmnf2 9924 pnfaddmnf 9925 mnfaddpnf 9926 xrex 9931 xltadd1 9951 xlt2add 9955 xsubge0 9956 xposdif 9957 xleaddadd 9962 elioc2 10011 elico2 10012 elicc2 10013 ioomax 10023 iccmax 10024 elioomnf 10043 unirnioo 10048 xrmaxadd 11426 reopnap 14782 blssioo 14789 tgioo 14790

W3C validator