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/c1be94e0-9b15-4918-bed7-39a366e1b0ccn%40googlegroups.com.
