@Benoît: yes, please move both theorems ~bj-eleq1w and ~bj-eleq2w to main
set.mm. I will shorten my proof afterwards. The following two lines
13 eleq2 $p |- ( e = c -> ( U e. e <-> U e. c ) )
14 13 cbvrabv $p |- { e e. E | U e. e } = { c e. E | U e. c }
will be replaced by
13 bj-eleq2w $p |- ( e = c -> ( U e. e <-> U e. c ) )
14 13 cbvrabv $p |- { e e. E | U e. e } = { c e. E | U e. c }
The number of steps (all 139, essential 23) of the whole proof will not be
decreased, but the number of bytes (especially if the prefix "bj-" is
removed).
On Saturday, December 12, 2020 at 7:32:11 PM UTC+1 Benoit wrote:
> Alexander: I'm pleasantly surprised that ~bj-eleq2w allows a minimization
> (probably avoiding a use of ~cv, compared to ~eleq2 ?). Its main goal is to
> reduce axiom dependencies (actually, that section of my mathbox shows how
> dependency on ~ax-ext, among others, can be removed from several dozens
> theorems --- yes, ~ax-ext is used in the eliminability theorem, but this is
> still interesting). If Norm agrees and you don't mind, I'll move it to
> Main, to its place, which is right after df-clel. Side note: ~bj-eleq2w
> actually uses fewer axioms than ~eleq2, since the latter does "morally" use
> ax-5--9 and ax-ext, as bj-dfclel and bj-dfcleq show.
>
> Benoît
>
--
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/a1cb6f37-06b1-4cf6-867a-578e31b45007n%40googlegroups.com.
