It's not clear to me why Norman used |- +oo = ~P U. CC
in place of the more straightforward ~P U. RR Below is a shorter proof of pnfnre (it uses a subset of the labels, then no more axioms) h50::pnfnre3.1 |- A = ~P U. RR 51:50:eleq1i |- ( A e. RR <-> ~P U. RR e. RR ) 52::pwuninel |- -. ~P U. RR e. RR 53:52,51:mtbir |- -. A e. RR qed:53:nelir |- A e/ RR Il giorno mercoledì 5 gennaio 2022 alle 22:04:44 UTC+1 [email protected] ha scritto: > On 1/5/22 11:54 AM, Glauco wrote: > > 1. the "standard" theory works perfectly fine without assuming plus > infinity not being a complex number. Thus, |- -. +oo e. CC should NOT be a > theorem in set.m > > As far as I could tell from a quick glance, everything would work if +oo > is defined to be _i and -oo is defined to be -u _i . > > At least that seems like it from the "requiring only that +∞ be a set not > in ℝ" language in http://us.metamath.org/mpeuni/df-pnf.html and, backing > it up, that df-pnf is only used in > http://us.metamath.org/mpeuni/pnfnre.html and > http://us.metamath.org/mpeuni/mnfnre.html (and a third one trivially > satisfied by anything used to define RR* the way we do) and that other > usages go via pnfnre . > > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3d27383e-b4a4-436e-9f4f-780c2fe7d605n%40googlegroups.com.
