Shorten axpr and reduce axiom usage

[LegionMammal978]

This PR shortens axpr by collapsing axprlem4 and axprlem5 into a common lemma, and also eliminates its usage of ax-9, ax-10, ax-11, and ax-12. In service of this, new theorems axrep4v (axrep4 with a DV condition in place of a not-free hypothesis, avoiding ax-12) and bm1.3iiv (extracted from bm1.3ii, avoiding ax-9) are added. The existing theorems axrep4, axrep6, and bm1.3ii are also shortened.

(Note that the non-usage of ax-8 could be considered a bit of a fiction, considering how either ax-8 or ax-12 is seemingly necessary in the proof of axsep. But it is what it is.)

[LegionMammal978]

I've revised bm1.3ii into a new theorem sepexi, which generalizes the conclusion of bm1.3ii while still avoiding ax-9. All users are adjusted for the extra syntax step. It is proved from a new closed-form sepex, which is proved from a weaker version sepexlem.

[benjub]

Thanks @avekens for the ping, since I'm following PRs here from further away these days.

So, after skimming through the changes: this PR extracts Step 12 of https://us.metamath.org/mpeuni/bj-bm1.3ii.html and proposes to move it to Main and to label it ~sepexlem (and then chains it with itself to remove the DV condition, and labels the result ~sepex). Indeed, the forward implication of ~bj-bm1.3ii uses fewer axioms than the whole biconditional, so it may be worth extracting it from its proof and moving it to Main, especially if it saves axioms later. The biconditional form ~bj-bm1.3ii is worth keeping.

[LegionMammal978]

Alright, in that case I've just replaced the "TODO" with "move after ~ sepexi".

Indeed, the forward implication of ~bj-bm1.3ii uses fewer axioms than the whole biconditional,

As it happens, it is possible to get the whole biconditional without adding axioms, by further chaining sepex with itself:

  ${
    $d x y $.  $d x z $.  $d ph y $.  $d ph z $.
    $( Biconditional form of ~ sepex .  (Contributed by Matthew House,
       26-Sep-2025.) $)
    sepexbi $p |- ( E. y A. x ( ph -> x e. y ) <->
        E. z A. x ( x e. z <-> ph ) ) $=
      ( wel wi wal wex wb sepex biimpr alimi eximi 3syl impbii ) ABCEZFZBGZCHZB
      DEZAIZBGZDHZABCDJUCATFZBGZDHPAIZBGZCHSUBUEDUAUDBTAKLMABDCJUGRCUFQBPAKLMNO
      $.
    $( $j usage 'sepexbi' avoids 'ax-9'; $)
  $}

 1 sepex      $p |- ( E. y A. x ( ph -> x e. y ) -> E. z A. x ( x e. z <-> ph ) )
 2 biimpr     $p |- ( ( x e. z <-> ph ) -> ( ph -> x e. z ) )
 3 2 alimi    $p |- ( A. x ( x e. z <-> ph ) -> A. x ( ph -> x e. z ) )
 4 3 eximi    $p |- ( E. z A. x ( x e. z <-> ph ) -> E. z A. x ( ph -> x e. z ) )
 5 sepex      $p |- ( E. z A. x ( ph -> x e. z ) -> E. y A. x ( x e. y <-> ph ) )
 6 biimpr     $p |- ( ( x e. y <-> ph ) -> ( ph -> x e. y ) )
 7 6 alimi    $p |- ( A. x ( x e. y <-> ph ) -> A. x ( ph -> x e. y ) )
 8 7 eximi    $p |- ( E. y A. x ( x e. y <-> ph ) -> E. y A. x ( ph -> x e. y ) )
 9 4,5,8 3syl $p |- ( E. z A. x ( x e. z <-> ph ) -> E. y A. x ( ph -> x e. y ) )
10 1,9 impbii $p |- ( E. y A. x ( ph -> x e. y ) <-> E. z A. x ( x e. z <-> ph ) )

[avekens]

I think it should be relabelled as "sepexbi", as proposed in the previous comment.

[wlammen]

@LegionMammal978 I suggest to resolve this comment, so I can merge the Pull request.