Thanks!
I was able to reach my objective using the rspcedvd variant (shouldn't
it be referenced from natded?), closer to my current proof setup \o/
```
d994::1red |- ( ph -> 1 e. RR )
d997::simpr |- ( ( ph /\ c = 1 ) -> c = 1 )
d998:d997:breq2d |- ( ( ph /\ c = 1 )
-> ( ( abs ` ( F ` x ) ) <_ c
<-> ( abs ` ( F ` x ) ) <_ 1 ) )
d995:d998:ralbidv |- ( ( ph /\ c = 1 )
-> ( A. x
e. RR
( abs ` ( F ` x ) ) <_ c
<-> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 ) )
exsup1:d994,d995,6:rspcedvd |- ( ph -> E. c e. RR A. x e. RR ( abs ` ( F
` x ) ) <_ c )
```
-stan
On Wed, Mar 4, 2020 at 5:46 PM Thierry Arnoux <[email protected]>
wrote:
> > Maybe I'm missing something but my high level goal is to prove:
> >
> > |- ( ph -> E. c e. RR A. x e. RR ( abs ` ( F ` x ) ) <_ c )
> >
> > using:
> >
> > |- ( ph -> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 )
> As pointed by Jim, the easier way to do this is to use ~rspcev and avoid
> the explicit substitution. You will need to prove:
>
> |- ( c = 1 -> ( A. x e. RR ( abs ` ( F ` x ) ) <_ c <-> A. x e. RR ( abs
> ` ( F ` x ) ) <_ 1 ) )
>
> In my case, MMJ2 often automatically fills in ~cbvral, but the right
> theorem for that step is ~ralbidv.
>
> --
> 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/e5d2f406-8edd-75fa-0fd9-9440affad7ab%40gmx.net
> .
>
--
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/CACZd_0x8Z7kNgMLx1tNNyk3eHH%3D_WBBdHb6VgHTxzCDPzsnwew%40mail.gmail.com.
