Hi Igor,
unfortunately, for a few days I'll not have the chance to test what I'm
writing, so take it with a grain of salt.
it makes the theorem less general, but we tend to write hyp5 without the
antecedent (as a "pure" local definition)
hyp5 |- F = ( x e. RR |-> ( ( K x. ( x ^ 2 ) ) + ( ( -u ( 2 x. K ) x. x ) +
L ) ) )
By writing
|- ( ph -> { x e. RR | ( F ` x ) = 4 } = { A , B } )
you are "stating" that { x e. RR | ( F ` x ) = 4 } has at most two
elements (I guess you don't want it in the hyp; maybe you can prove it, but
you don't want it in a hyp)
In place of hyp 6,7,8 You probably want something like
|- X = { x e. RR | ( F ` x ) = 4 }
|- ( ph -> A e. X )
|- ( ph -> B e. X )
In both cases, with hyp9 you can prove that A =/= B
--
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 visit
https://groups.google.com/d/msgid/metamath/be8d6973-8d1f-41f6-be9c-b9f58b75ccaan%40googlegroups.com.
