You should read any statement starting |- and having a set variable in it as universally quantified over those variables. So when you see |- 0 < k that's saying "0 < k is derivable in the empty context" which is a strong statement, equivalent to "for all k, 0 < k" which is of course false.
On Sun, Oct 20, 2024 at 10:01 AM Igor Ieskov <[email protected]> wrote: > Thanks Glauco for showing this example. I didn’t expect that |- 0 < k > implies |- 0 < -u 1 . > > > - > > Igor > > On Saturday, October 19, 2024 at 8:29:25 PM UTC+2 Glauco wrote: > >> Hi Igor, >> >> as Mario pointed out, we'd better be careful with free setvars in hyps. >> >> For instance, from hyp >> >> |- 0 < k >> >> you can derive everything. Here's an example >> >> h1::temp4.1 |- 0 < k >> 2::negex |- -u 1 e. _V >> 3::breq2 |- ( k = -u 1 -> ( 0 < k <-> 0 < -u 1 ) ) >> 4:2,3,1:vtocl |- 0 < -u 1 >> 5::lenlt |- ( ( -u 1 e. RR /\ 0 e. RR ) -> ( -u 1 <_ 0 <-> >> -. 0 < -u 1 ) ) >> 6::neg1rr |- -u 1 e. RR >> 7::0re |- 0 e. RR >> 8::neg1lt0 |- -u 1 < 0 >> 9:6,7,8:ltleii |- -u 1 <_ 0 >> 10::neg1rr |- -u 1 e. RR >> 11::0re |- 0 e. RR >> 12:10,11,5:mp2an |- ( -u 1 <_ 0 <-> -. 0 < -u 1 ) >> 13:12:biimpi |- ( -u 1 <_ 0 -> -. 0 < -u 1 ) >> 14:9,13:ax-mp |- -. 0 < -u 1 >> qed:4,14:pm2.24ii |- 1 e. (/) >> >> $= ( cc0 c1 cneg clt wbr c0 wcel cv negex breq2 vtocl cle wn neg1rr 0re >> neg1lt0 >> ltleii cr wb lenlt mp2an biimpi ax-mp pm2.24ii ) >> CDEZFGZDHICAJZFGUHAUGDKUIUG >> CFLBMUGCNGZUHOZUGCPQRSUJUKUGTICTIUJUKUAPQUGCUBUCUDUEUF $. >> >> >> -- > 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/3bf568bf-cae2-4853-9735-555598676ef5n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/3bf568bf-cae2-4853-9735-555598676ef5n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSsNA%2Bya%2BXxp%3DjjtNgOp%2BzwdSi5jX-W2LwJuApouwSDzRw%40mail.gmail.com.
