mnfxr - Intuitionistic Logic Explorer

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

Theorem mnfxr 8100

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 8081	. . . . 5 ⊢ -∞ = 𝒫 +∞
2		pnfex 8097	. . . . . 6 ⊢ +∞ ∈ V
3	2	pwex 4217	. . . . 5 ⊢ 𝒫 +∞ ∈ V
4	1, 3	eqeltri 2269	. . . 4 ⊢ -∞ ∈ V
5	4	prid2 3730	. . 3 ⊢ -∞ ∈ {+∞, -∞}
6		elun2 3332	. . 3 ⊢ (-∞ ∈ {+∞, -∞} → -∞ ∈ (ℝ ∪ {+∞, -∞}))
7	5, 6	ax-mp 5	. 2 ⊢ -∞ ∈ (ℝ ∪ {+∞, -∞})
8		df-xr 8082	. 2 ⊢ ℝ^* = (ℝ ∪ {+∞, -∞})
9	7, 8	eleqtrri 2272	1 ⊢ -∞ ∈ ℝ^*

Colors of variables: wff set class

Syntax hints: ∈ wcel 2167 Vcvv 2763 ∪ cun 3155 𝒫 cpw 3606 {cpr 3624 ℝcr 7895 +∞cpnf 8075 -∞cmnf 8076 ℝ^*cxr 8077

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 4152 ax-pow 4208 ax-un 4469 ax-cnex 7987

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 3608 df-sn 3629 df-pr 3630 df-uni 3841 df-pnf 8080 df-mnf 8081 df-xr 8082

This theorem is referenced by: elxr 9868 xrltnr 9871 mnflt 9875 mnfltpnf 9877 nltmnf 9880 mnfle 9884 xrltnsym 9885 xrlttri3 9889 ngtmnft 9909 xrrebnd 9911 xrre2 9913 xrre3 9914 ge0gtmnf 9915 xnegcl 9924 xltnegi 9927 xaddf 9936 xaddval 9937 xaddmnf1 9940 xaddmnf2 9941 pnfaddmnf 9942 mnfaddpnf 9943 xrex 9948 xltadd1 9968 xlt2add 9972 xsubge0 9973 xposdif 9974 xleaddadd 9979 elioc2 10028 elico2 10029 elicc2 10030 ioomax 10040 iccmax 10041 elioomnf 10060 unirnioo 10065 xrmaxadd 11443 reopnap 14866 blssioo 14873 tgioo 14874

W3C validator