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/6a666b51-352c-4edc-bd72-8dc67c65c7e1%40googlegroups.com.
