On Tuesday, December 28, 2021 at 3:08:36 AM UTC+1 [email protected]
wrote:
> I often want to use substitution to do something like this:
> |- ph & |- x = y |- ( [ y / x ] ph <-> ps ) ==> |- ps
> But I'm having trouble showing that ps results from the proper
> substitution of y for x in ph.
>
What is the problem with Brian's theorem? A proof of it (mainly based on
~sbequ12) is as follows:
sbiei.1 $e |- ph $.
sbiei.2 $e |- x = y $.
sbiei.3 $e |- ( [ y / x ] ph <-> ps ) $.
sbiei $p |- ps $=
1 sbiei.1 $e |- ph
2 sbiei.2 $e |- x = y
3 sbequ12 $p |- ( x = y -> ( ph <-> [ y / x ] ph ) )
4 2,3 ax-mp $a |- ( ph <-> [ y / x ] ph )
5 1,4 mpbi $p |- [ y / x ] ph
6 sbiei.3 $e |- ( [ y / x ] ph <-> ps )
7 5,6 mpbi $p |- ps
Even in closed form the theorem is valid:
sbieg $p |- ( ( ph /\ x = y /\ ( [ y / x ] ph <-> ps ) ) -> ps ) $=
1 bicom $p |- ( ( ps <-> ph ) <-> ( ph <-> ps ) )
2 sbequ12 $p |- ( x = y -> ( ph <-> [ y / x ] ph ) )
3 2 bibi1d $p |- ( x = y -> ( ( ph <-> ps ) <-> ( [ y / x ] ph <-> ps
) ) )
4 3 adantl $p |- ( ( ph /\ x = y ) -> ( ( ph <-> ps ) <-> ( [ y / x ]
ph <-> ps ) ) )
5 1,4 syl5bb $p |- ( ( ph /\ x = y ) -> ( ( ps <-> ph ) <-> ( [ y / x ]
ph <-> ps ) ) )
6 bianir $p |- ( ( ph /\ ( ps <-> ph ) ) -> ps )
7 6 ex $p |- ( ph -> ( ( ps <-> ph ) -> ps ) )
8 7 adantr $p |- ( ( ph /\ x = y ) -> ( ( ps <-> ph ) -> ps ) )
9 5,8 sylbird $p |- ( ( ph /\ x = y ) -> ( ( [ y / x ] ph <-> ps ) -> ps
) )
10 9 3impia $p |- ( ( ph /\ x = y /\ ( [ y / x ] ph <-> ps ) ) -> ps )
--
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/3552df55-5fa8-4c22-9cc4-dedf0ecde0efn%40googlegroups.com.
