Hello all,
I was practicing some proof shortening skills and I came across this proof
for cnfex that accomplishes it in 2 steps rather than the original 20,
Original:
$d f y J $. $d f y K $.
cnfex $p |- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V ) $=
( vf vy ctop wcel wa co cuni cvv ctopon cfv wceq eqid jctr istopon sylibr
cv syl2an uniexg ccn ccnv cima wral cmap crab cnfval wf cab mapvalg mapex
syl2anr eqeltrd rabexg syl )
AEFZBEFZGZABUAHZCRZUBDRUCAFDBUDZCBIZAIZUEHZUFZJUPAVCKLFZBVBKLFZUSVEMUQUPUPVCVCMZGVFUPVHVCNOVCAPQUQUQVBVBMZGVGUQVIVBNOVBBPQDCABVCVBUGSURVDJFVEJFURVDVCVBUTUHCUIZJUQVBJFZVCJFZVDVJMUPBETZAETZVBVCJJCUJULUPVLVKVJJFUQVNVMVCVBJJCUKSUMVACVDJUNUOUM
$.
Shortened:
cnfex $p |- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V ) $=
( ccn co cvv wcel ctop wa ovex a1i ) ABCDEFAGFBGFHABCIJ $.
I was wondering if this shortening was valid, as it gets rid of the two
dummy variables originally used, and just seems too good to be true for an
originally, fairly large proof.
Can anyone comment on whether this shortening is valid? At least Metamath
seems to think so.
Thanks,
--
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/f756107b-2a48-47a3-a0e6-9a590f4ed0cdn%40googlegroups.com.
