This is done in PR #1604 (https://github.com/metamath/set.mm/pull/1604). Feel free to shorten some proofs and add credits. By the way: I like your theorems using if- . I think that you can add this one: ( ph /\ ps ) <-> if- ( ph , ps , ph ) it is to ~bj-ifdfan what ~bj-ifdfor2 is to ~bj-ifdfor. And consequently: if- ( ph , ps , ph ) <-> if- ( ps , ph , ps )
Benoît On Thursday, April 23, 2020 at 9:33:50 AM UTC+2, Richard Penner wrote: > > Ah. Well my proof of dfifp3 is necessarily longer than that of bj-dfif3 > which relies on bj-dfif2 to do half the work. > > The main problem I had with simply swapping bj-dfif5 and df-bj-if is > that bj-dfif2 and bj-dfif4 use df-bj-if directly which means to preserve > both their proofs and their numbering (other than the definition and "5"), > the proofs would have to come in an order corresponding with the partial > order (df) -> 5 -> 2 -> 3 , (df) -> 5 -> 4 , (df) -> 6 -> 7 ; Say (df) -> > 5 -> 2 -> 3 -> 4 -> 6 -> 7. > > You might be OK with that or you might want to have an ordering consistent > with numbering, in which case we need to free up the dependency of 2 and 4 > on 5. > > So here is a proof of bj-dfif2 in terms of bj-dfif5 as df-ifp > > ( wif wa wn wo wi df-ifp cases2 pm4.64 anbi2i 3bitri ) > ABCDABEAFZCEGABHZNCH > ZEOACGZEABCIABCJPQOACKLM $. > > and here is a proof of bj-dfif4 in terms of bj-dfif5 as df-ifp > > ( wif wa wn wo wi df-ifp cases2 imor anbi1i 3bitri ) > ABCDABEAFZCEGABHZNCHZE > NBGZPEABCIABCJOQPABKLM $. > > Good luck with the move. > > -- 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/83c5a89f-5024-4d89-ae6b-303d0c797f00%40googlegroups.com.
