It is certainly valid as long as ovex is valid. In Metamath the result of any function evaluated on a class is a set, as shown by fvex, so this extends to operations as well, no matter how complicated. It seems the original proof unnecessarily expanded on the meaning of Cn, when its use as an operation was sufficient to complete the proof.
On Wed, Apr 21, 2021 at 6:08 PM Kyle Wyonch <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/f756107b-2a48-47a3-a0e6-9a590f4ed0cdn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAPtOB9NvmC4FP2Skw2JAZhyREXf2Y8QRWKi8JS9-UJ9VDHYKrQ%40mail.gmail.com.
