Reduce ax-pow usage in php corollaries

discouraged

@@ -18082,6 +18082,7 @@ New usage of "nmoxr" is discouraged (7 uses).
 New usage of "nn0ge2m1nnALT" is discouraged (0 uses).
 New usage of "nn0indALT" is discouraged (3 uses).
 New usage of "nnadjuALT" is discouraged (0 uses).
+New usage of "nndomogOLD" is discouraged (0 uses).
 New usage of "nneneqOLD" is discouraged (1 uses).
 New usage of "nnexALT" is discouraged (3 uses).
 New usage of "nnfiOLD" is discouraged (0 uses).
@@ -18383,9 +18384,12 @@ New usage of "phnv" is discouraged (18 uses).
 New usage of "phnvi" is discouraged (22 uses).
 New usage of "phoeqi" is discouraged (1 uses).
 New usage of "phop" is discouraged (1 uses).
+New usage of "php2OLD" is discouraged (0 uses).
+New usage of "php3OLD" is discouraged (0 uses).
 New usage of "phpOLD" is discouraged (0 uses).
 New usage of "phpar" is discouraged (2 uses).
 New usage of "phpar2" is discouraged (2 uses).
+New usage of "phpeqdOLD" is discouraged (0 uses).
 New usage of "phplem1OLD" is discouraged (1 uses).
 New usage of "phplem2OLD" is discouraged (1 uses).
 New usage of "phplem3OLD" is discouraged (2 uses).
@@ -20882,6 +20886,7 @@ Proof modification of "nmounbseqiALT" is discouraged (146 steps).
 Proof modification of "nn0ge2m1nnALT" is discouraged (48 steps).
 Proof modification of "nn0indALT" is discouraged (15 steps).
 Proof modification of "nnadjuALT" is discouraged (62 steps).
+Proof modification of "nndomogOLD" is discouraged (97 steps).
 Proof modification of "nneneqOLD" is discouraged (459 steps).
 Proof modification of "nnexALT" is discouraged (34 steps).
 Proof modification of "nnfiOLD" is discouraged (14 steps).
@@ -20949,7 +20954,10 @@ Proof modification of "peano5OLD" is discouraged (304 steps).
 Proof modification of "perfectALTV" is discouraged (528 steps).
 Proof modification of "permsetexOLD" is discouraged (42 steps).
 Proof modification of "perpdragALT" is discouraged (241 steps).
+Proof modification of "php2OLD" is discouraged (110 steps).
+Proof modification of "php3OLD" is discouraged (463 steps).
 Proof modification of "phpOLD" is discouraged (378 steps).
+Proof modification of "phpeqdOLD" is discouraged (77 steps).
 Proof modification of "phplem1OLD" is discouraged (70 steps).
 Proof modification of "phplem2OLD" is discouraged (173 steps).
 Proof modification of "phplem3OLD" is discouraged (82 steps).

set.mm

@@ -92155,44 +92155,47 @@ proved without using the Axiom of Power Sets (unlike ~ domsdomtr ).
     $( $j usage 'php' avoids 'ax-pow'; $)
   $}
 
-  ${
-    $d x y A $.  $d x y B $.
-    $( Corollary of Pigeonhole Principle.  (Contributed by NM, 31-May-1998.) $)
-    php2 $p |- ( ( A e. _om /\ B C. A ) -> B ~< A ) $=
-      ( vx com wcel wpss csdm wbr cv wa wceq eleq1 psseq2 anbi12d breq2 imbi12d
-      wi cdom cen cvv wss vex pssss ssdomg mpsyl adantl php ensym nsyl sylanbrc
-      wn brsdom vtoclg anabsi5 ) ADEZBAFZBAGHZCIZDEZBURFZJZBURGHZQUOUPJZUQQCADU
-      RAKZVAVCVBUQVDUSUOUTUPURADLURABMNURABGOPVABURRHZBURSHZUKVBUTVEUSURTEUTBUR
-      UAVECUBBURUCBURTUDUEUFVAURBSHVFURBUGBURUHUIBURULUJUMUN $.
-  $}
+  $( Corollary of Pigeonhole Principle.  (Contributed by NM, 31-May-1998.)
+     Avoid ~ ax-pow .  (Revised by BTernaryTau, 20-Nov-2024.) $)
+  php2 $p |- ( ( A e. _om /\ B C. A ) -> B ~< A ) $=
+    ( com wcel wpss wa cdom wbr cen wn csdm cfn wss nnfi ssdomfi imp syl2an php
+    pssss wi ensymfib biimprd syl adantr mtod brsdom sylanbrc ) ACDZBAEZFZBAGHZ
+    BAIHZJBAKHUHALDZBAMZUKUIANZBASUMUNUKBAOPQUJULABIHZABRUHULUPTZUIUHUMUQUOUMUP
+    ULABUAUBUCUDUEBAUFUG $.
+  $( $j usage 'php2' avoids 'ax-pow'; $)
 
   ${
-    $d f x y A $.  $d f x y B $.
+    $d A f x y $.  $d B f x y $.
     $( Corollary of Pigeonhole Principle.  If ` A ` is finite and ` B ` is a
        proper subset of ` A ` , the ` B ` is strictly less numerous than
        ` A ` .  Stronger version of Corollary 6C of [Enderton] p. 135.
-       (Contributed by NM, 22-Aug-2008.) $)
+       (Contributed by NM, 22-Aug-2008.)  Avoid ~ ax-pow .  (Revised by
+       BTernaryTau, 26-Nov-2024.) $)
     php3 $p |- ( ( A e. Fin /\ B C. A ) -> B ~< A ) $=
-      ( vx vf vy wcel wpss wbr cv cen com wi wa wn wss imp wf1o wex cima syl c0
-      cfn csdm wrex isfi cvv relen brrelex1i pssss ssdomg syl2an adantll imass2
-      cdom bren adantl cdif pssnel eldif cfv f1ofn difss fnfvima 3expia sylancl
-      wceq wfn wfo ccnv wfun dff1o3 imadif simplbiim eleq2d sylibd syl6 syl5bir
-      n0i exlimdv sylan2 ssdif0 sylnibr dfpss3 sylanbrc cdm crn imadmrn imaeq2d
-      wb f1odm f1ofo forn 3eqtr3a psseq2d adantr mpbid php wf1 f1of1 f1ores vex
-      cres resex f1oeq1 spcev sylibr entr expcom mtod exp32 imp31 ensym syl6com
-      syl5bi ex ad2antlr brsdom exp31 rexlimiv sylbi ) AUBFZBAGZBAUCHZYAACIZJHZ
-      CKUDYBYCLZCAUEYEYFCKYDKFZYEYBYCYGYEMYBMZBAUNHZBAJHZNYCYEYBYIYGYEAUFFZBAOZ
-      YIYBAYDJUGUHBAUIZYKYLYIBAUFUJPUKULYHYJYDBJHZYGYEYBYNNZYEAYDDIZQZDRYGYBYOL
-      ZAYDDUOYGYQYRDYGYQYBYOYGYQYBMZMYNYDYPBSZJHZYSYGYTYDGZUUANYSYTYPASZGZUUBYS
-      YTUUCOZUUCYTOZNUUDYBUUEYQYBYLUUEYMBAYPUMTUPYSUUCYTUQZUAVFZUUFYBYQEIZAFUUI
-      BFNMZERZUUHNZEBAURYQUUKUULYQUUJUULEUUJUUIABUQZFZYQUULUUIABUSYQUUNUUIYPUTZ
-      UUGFZUULYQUUNUUOYPUUMSZFZUUPYQYPAVGZUUMAOZUUNUURLAYDYPVAABVBUUSUUTUUNUURA
-      UUMYPUUIVCVDVEYQUUQUUGUUOYQAYDYPVHZYPVIVJUUQUUGVFAYDYPVKABYPVLVMVNVOUUGUU
-      OVRVPVQVSPVTUUCYTWAWBYTUUCWCWDYQUUDUUBWIYBYQUUCYDYTYQYPYPWEZSYPWFZUUCYDYP
-      WGYQUVBAYPAYDYPWJWHYQUVAUVCYDVFAYDYPWKAYDYPWLTWMWNWOWPYDYTWQVTYSYNUUALZYG
-      YSBYTJHZUVDYSBYTYPBXBZQZUVEYQAYDYPWRYLUVGYBAYDYPWSYMAYDBYPWTUKUVGBYTUUIQZ
-      ERUVEUVHUVGEUVFYPBDXAXCBYTUUIUVFXDXEBYTEUOXFTYNUVEUUAYDBYTXGXHTUPXIXJVSXN
-      XKYEYJYNLYGYBYJYEBYDJHZYNYJYEUVIBAYDXGXOBYDXLXMXPXIBAXQWDXRXSXTP $.
+      ( vx vf vy cfn wcel wpss csdm wbr cv cen com wi wf1o wex cima sylan2 cdom
+      wss wrex isfi bren wa wn pssss imass2 syl adantl cdif c0 pssnel eldif cfv
+      wceq f1ofn difss fnfvima 3expia sylancl ccnv wfun dff1o3 imadif simplbiim
+      wfn wfo eleq2d sylibd n0i syl6 syl5bir exlimdv imp ssdif0 dfpss3 sylanbrc
+      sylnibr wb cdm crn imadmrn f1odm imaeq2d f1ofo forn 3eqtr3a psseq2d mpbid
+      adantr php2 nnfi cres f1of1 f1ores syl2an resex f1oeq1 spcev sylibr endom
+      wf1 vex sdomdom domfi 3adant2 3adant3 domsdomtrfi syld3an1 syl3an2 syl5bi
+      exp32 ensymfib biimp3ar sdomdomtrfi syl3an3 syld3an3 syl3an1 3com23 syldd
+      mpd 3exp rexlimiv sylbi ) AFGZBAHZBAIJZYEACKZLJZCMUAYFYGNZCAUBYIYJCMYHMGZ
+      YIYFBYHIJZYGYIAYHDKZOZDPYKYFYLNZAYHDUCYKYNYODYKYNYFYLYKYNYFUDZUDYMBQZYHIJ
+      ZYLYPYKYQYHHZYRYPYQYMAQZHZYSYPYQYTTZYTYQTZUEUUAYFUUBYNYFBATZUUBBAUFZBAYMU
+      GUHUIYPYTYQUJZUKUOZUUCYFYNEKZAGUUHBGUEUDZEPZUUGUEZEBAULYNUUJUUKYNUUIUUKEU
+      UIUUHABUJZGZYNUUKUUHABUMYNUUMUUHYMUNZUUFGZUUKYNUUMUUNYMUULQZGZUUOYNYMAVFZ
+      UULATZUUMUUQNAYHYMUPABUQUURUUSUUMUUQAUULYMUUHURUSUTYNUUPUUFUUNYNAYHYMVGZY
+      MVAVBUUPUUFUOAYHYMVCABYMVDVEVHVIUUFUUNVJVKVLVMVNRYTYQVOVRYQYTVPVQYNUUAYSV
+      SYFYNYTYHYQYNYMYMVTZQYMWAZYTYHYMWBYNUVAAYMAYHYMWCWDYNUUTUVBYHUOAYHYMWEAYH
+      YMWFUHWGWHWJWIYHYQWKRYKYHFGZBYQLJZYRYLNYPYHWLZYPBYQYMBWMZOZUVDYNAYHYMXBUU
+      DUVGYFAYHYMWNUUEAYHBYMWOWPUVGBYQUUHOZEPUVDUVHUVGEUVFYMBDXCWQBYQUUHUVFWRWS
+      BYQEUCWTUHUVCUVDYRYLUVDUVCBYQSJZYRYLBYQXAYQFGZUVIUVCYRYLUVCYRUVJUVIYRUVCY
+      QYHSJUVJYQYHXDYHYQXERXFBFGZUVIUVJYRYLUVJUVIUVKYRYQBXEXGBYQYHXHXIXIXJUSWPY
+      AXLVMXKYKYIYLYGYKYLYIYGYKUVCYLYIYGUVEUVCYLYIYHALJZYGUVCYLUVLYIUVCUVLYIVSY
+      LYHAXMWJXNUVLUVCYLYHASJZYGYHAXAUVKYLUVCUVMYGUVCYLUVKUVMYLUVCBYHSJUVKBYHXD
+      YHBXERXGBYHAXOXIXPXQXRXSYBXTYCYDVN $.
+    $( $j usage 'php3' avoids 'ax-pow'; $)
   $}
 
   $( Corollary of the Pigeonhole Principle ~ php : a natural number is strictly
@@ -92214,12 +92217,13 @@ proved without using the Axiom of Power Sets (unlike ~ domsdomtr ).
     phpeqd.3 $e |- ( ph -> A ~~ B ) $.
     $( Corollary of the Pigeonhole Principle using equality.  Strengthening of
        ~ php expressed without negation.  (Contributed by Rohan Ridenour,
-       3-Aug-2023.) $)
+       3-Aug-2023.)  Avoid ax-pow.  (Revised by BTernaryTau, 28-Nov-2024.) $)
     phpeqd $p |- ( ph -> A = B ) $=
-      ( cen wbr wceq wn wa csdm cfn wcel wpss wss adantr simpr neqcomd dfpss2
-      sylanbrc php3 syl2an2r sdomnen ensym nsyl syl ex mt4d ) ABCGHZBCIZFAUKJZU
-      JJZAULKZCBLHZUMABMNULCBOZUODUNCBPZCBIJUPAUQULEQUNBCAULRSCBTUABCUBUCUOCBGH
-      UJCBUDBCUEUFUGUHUI $.
+      ( cen wbr wceq wn csdm cfn wcel wpss wa wss adantr simpr neqcomd dfpss2
+      sylanbrc php3 syl2an2r sdomnen ensymfib notbid biimpar syl2an syldan mt4d
+      ex ) ABCGHZBCIZFAUMJZULJZAUNCBKHZUOABLMZUNCBNZUPDAUNOZCBPZCBIJURAUTUNEQUS
+      BCAUNRSCBTUABCUBUCAUQCBGHZJZUOUPDCBUDUQUOVBUQULVABCUEUFUGUHUIUKUJ $.
+    $( $j usage 'phpeqd' avoids 'ax-pow'; $)
   $}
 
   $( A singleton ` { A } ` is never equinumerous with the ordinal number 2.
@@ -92235,13 +92239,16 @@ being the empty set ( ` A e/ _V ` ).  (Contributed by AV, 6-Aug-2019.) $)
   $( Cardinal ordering agrees with ordinal number ordering when the smaller
      number is a natural number.  Compare with ~ nndomo when both are natural
      numbers.  (Contributed by NM, 17-Jun-1998.)  Generalize from ~ nndomo .
-     (Revised by RP, 5-Nov-2023.) $)
+     (Revised by RP, 5-Nov-2023.)  Avoid ~ ax-pow .  (Revised by BTernaryTau,
+     29-Nov-2024.) $)
   nndomog $p |- ( ( A e. _om /\ B e. On ) -> ( A ~<_ B <-> A C_ B ) ) $=
-    ( com wcel con0 wa cdom wbr wss wpss wn wi csdm php2 ex domnsym adantr word
-    nsyli wb ordtri1 ordelpss ancoms notbid syl2an sylibrd ssdomg adantl impbid
-    nnord eloni bitrd ) ACDZBEDZFZABGHZABIZUOUPBAJZKZUQUMUPUSLUNUMURBAMHZUPUMUR
-    UTABNOABPSQUMARZBRZUQUSTUNAUJBUKVAVBFZUQBADZKUSABUAVCVDURVBVAVDURTBAUBUCUDU
-    LUEUFUNUQUPLUMABEUGUHUI $.
+    ( com wcel con0 wa cdom wbr wss wpss wn wi csdm cfn nnfi domnsymfi sylan ex
+    word wb php2 nsyld adantr nnord eloni ordtri1 ordelpss ancoms notbid syl2an
+    bitrd sylibrd ssdomfi2 3expia impbid ) ACDZBEDZFZABGHZABIZURUSBAJZKZUTUPUSV
+    BLUQUPUSBAMHZVAUPUSVCKZUPANDZUSVDAOZABPQRUPVAVCABUARUBUCUPASZBSZUTVBTUQAUDB
+    UEVGVHFZUTBADZKVBABUFVIVJVAVHVGVJVATBAUGUHUIUKUJULUPVEUQUTUSLVFVEUQUTUSABEU
+    MUNQUO $.
+  $( $j usage 'nndomog' avoids 'ax-pow'; $)
 
   $( Obsolete lemma for ~ php .  (Contributed by NM, 25-May-1998.)
      (Proof modification is discouraged.)  (New usage is discouraged.) $)
@@ -92349,6 +92356,71 @@ being the empty set ( ` A e/ _V ` ).  (Contributed by AV, 6-Aug-2019.) $)
       KYCAXOBHXAXBXCXDXEXFXGXHT $.
   $}
 
+  ${
+    $d x y A $.  $d x y B $.
+    $( Obsolete version of ~ php2 as of 20-Nov-2024.  (Contributed by NM,
+       31-May-1998.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    php2OLD $p |- ( ( A e. _om /\ B C. A ) -> B ~< A ) $=
+      ( vx com wcel wpss csdm wbr cv wa wceq eleq1 psseq2 anbi12d breq2 imbi12d
+      wi cdom cen cvv wss vex pssss ssdomg mpsyl adantl php ensym nsyl sylanbrc
+      wn brsdom vtoclg anabsi5 ) ADEZBAFZBAGHZCIZDEZBURFZJZBURGHZQUOUPJZUQQCADU
+      RAKZVAVCVBUQVDUSUOUTUPURADLURABMNURABGOPVABURRHZBURSHZUKVBUTVEUSURTEUTBUR
+      UAVECUBBURUCBURTUDUEUFVAURBSHVFURBUGBURUHUIBURULUJUMUN $.
+  $}
+
+  ${
+    $d f x y A $.  $d f x y B $.
+    $( Obsolete version of ~ php3 as of 26-Nov-2024.  (Contributed by NM,
+       22-Aug-2008.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    php3OLD $p |- ( ( A e. Fin /\ B C. A ) -> B ~< A ) $=
+      ( vx vf vy wcel wpss wbr cv cen com wi wa wn wss imp wf1o wex cima syl c0
+      cfn csdm wrex isfi cvv relen brrelex1i pssss ssdomg syl2an adantll imass2
+      cdom bren adantl cdif pssnel eldif cfv f1ofn difss fnfvima 3expia sylancl
+      wceq wfn wfo ccnv wfun dff1o3 imadif simplbiim eleq2d sylibd syl6 syl5bir
+      n0i exlimdv sylan2 ssdif0 sylnibr dfpss3 sylanbrc cdm crn imadmrn imaeq2d
+      wb f1odm f1ofo forn 3eqtr3a psseq2d adantr mpbid php wf1 f1of1 f1ores vex
+      cres resex f1oeq1 spcev sylibr entr expcom mtod exp32 imp31 ensym syl6com
+      syl5bi ex ad2antlr brsdom exp31 rexlimiv sylbi ) AUBFZBAGZBAUCHZYAACIZJHZ
+      CKUDYBYCLZCAUEYEYFCKYDKFZYEYBYCYGYEMYBMZBAUNHZBAJHZNYCYEYBYIYGYEAUFFZBAOZ
+      YIYBAYDJUGUHBAUIZYKYLYIBAUFUJPUKULYHYJYDBJHZYGYEYBYNNZYEAYDDIZQZDRYGYBYOL
+      ZAYDDUOYGYQYRDYGYQYBYOYGYQYBMZMYNYDYPBSZJHZYSYGYTYDGZUUANYSYTYPASZGZUUBYS
+      YTUUCOZUUCYTOZNUUDYBUUEYQYBYLUUEYMBAYPUMTUPYSUUCYTUQZUAVFZUUFYBYQEIZAFUUI
+      BFNMZERZUUHNZEBAURYQUUKUULYQUUJUULEUUJUUIABUQZFZYQUULUUIABUSYQUUNUUIYPUTZ
+      UUGFZUULYQUUNUUOYPUUMSZFZUUPYQYPAVGZUUMAOZUUNUURLAYDYPVAABVBUUSUUTUUNUURA
+      UUMYPUUIVCVDVEYQUUQUUGUUOYQAYDYPVHZYPVIVJUUQUUGVFAYDYPVKABYPVLVMVNVOUUGUU
+      OVRVPVQVSPVTUUCYTWAWBYTUUCWCWDYQUUDUUBWIYBYQUUCYDYTYQYPYPWEZSYPWFZUUCYDYP
+      WGYQUVBAYPAYDYPWJWHYQUVAUVCYDVFAYDYPWKAYDYPWLTWMWNWOWPYDYTWQVTYSYNUUALZYG
+      YSBYTJHZUVDYSBYTYPBXBZQZUVEYQAYDYPWRYLUVGYBAYDYPWSYMAYDBYPWTUKUVGBYTUUIQZ
+      ERUVEUVHUVGEUVFYPBDXAXCBYTUUIUVFXDXEBYTEUOXFTYNUVEUUAYDBYTXGXHTUPXIXJVSXN
+      XKYEYJYNLYGYBYJYEBYDJHZYNYJYEUVIBAYDXGXOBYDXLXMXPXIBAXQWDXRXSXTP $.
+  $}
+
+  ${
+    phpeqdOLD.1 $e |- ( ph -> A e. Fin ) $.
+    phpeqdOLD.2 $e |- ( ph -> B C_ A ) $.
+    phpeqdOLD.3 $e |- ( ph -> A ~~ B ) $.
+    $( Obsolete version of ~ phpeqd as of 28-Nov-2024.  (Contributed by Rohan
+       Ridenour, 3-Aug-2023.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    phpeqdOLD $p |- ( ph -> A = B ) $=
+      ( cen wbr wceq wn wa csdm cfn wcel wpss wss adantr simpr neqcomd dfpss2
+      sylanbrc php3 syl2an2r sdomnen ensym nsyl syl ex mt4d ) ABCGHZBCIZFAUKJZU
+      JJZAULKZCBLHZUMABMNULCBOZUODUNCBPZCBIJUPAUQULEQUNBCAULRSCBTUABCUBUCUOCBGH
+      UJCBUDBCUEUFUGUHUI $.
+  $}
+
+  $( Obsolete version of ~ nndomog as of 29-Nov-2024.  (Contributed by NM,
+     17-Jun-1998.)  Generalize from ~ nndomo .  (Revised by RP, 5-Nov-2023.)
+     (Proof modification is discouraged.)  (New usage is discouraged.) $)
+  nndomogOLD $p |- ( ( A e. _om /\ B e. On ) -> ( A ~<_ B <-> A C_ B ) ) $=
+    ( com wcel con0 wa cdom wbr wss wpss wn wi csdm php2 ex domnsym adantr word
+    nsyli wb ordtri1 ordelpss ancoms notbid syl2an sylibrd ssdomg adantl impbid
+    nnord eloni bitrd ) ACDZBEDZFZABGHZABIZUOUPBAJZKZUQUMUPUSLUNUMURBAMHZUPUMUR
+    UTABNOABPSQUMARZBRZUQUSTUNAUJBUKVAVBFZUQBADZKUSABUAVCVDURVBVAVDURTBAUBUCUDU
+    LUEUFUNUQUPLUMABEUGUHUI $.
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=