Intuitionize recent set.mm theorems (metamath#3750)

* Add phpeqd to iset.mm Stated as in set.mm. The proof is immediate from fisseneq which we already have. * Add phphashd and phphashrd to mmil.html * Add neqcomd to iset.mm Copied without change from set.mm. * Add hashelne0d to mmil.html * add hash1elsn to mmil.html * Add gcdmultipled to iset.mm Copied without change from set.mm * Add dvdsgcdidd to iset.mm Stated as in set.mm. The proof needs a very small amount of intuitionizing but is basically the set.mm proof. * Add rspcime to iset.mm Copied without change from set.mm * Add elrnmptdv to iset.mm Copied without change from set.mm * Add elrnmpt2d to iset.mm Copied without change from set.mm * Add enpr2d to iset.mm Copied without change from set.mm
avekens · Jan 7, 2024 · f42e3e5 · f42e3e5
1 parent de46203
commit f42e3e5
Show file tree

Hide file tree

Showing 2 changed files with 109 additions and 0 deletions.
diff --git a/iset.mm b/iset.mm
@@ -18169,6 +18169,13 @@ This law is thought to have originated with Aristotle (_Metaphysics_,
       ( wceq eqcom mpbi ) ABDBADCABEF $.
   $}
 
+  ${
+    neqcomd.1 $e |- ( ph -> -. A = B ) $.
+    $( Commute an inequality.  (Contributed by Rohan Ridenour, 3-Aug-2023.) $)
+    neqcomd $p |- ( ph -> -. B = A ) $=
+      ( wceq eqcom sylnib ) ABCECBEDBCFG $.
+  $}
+
   ${
     eqcomd.1 $e |- ( ph -> A = B ) $.
     $( Deduction from commutative law for class equality.  (Contributed by NM,
@@ -23933,6 +23940,16 @@ deduction version (Contributed by Thierry Arnoux, 30-Jan-2017.) $)
       ( wrex rspcedv mpd ) ACBDFJIABCDEFGHKL $.
   $}
 
+  ${
+    $d x ph $.  $d x B $.  $d x A $.
+    rspcime.1 $e |- ( ( ph /\ x = A ) -> ps ) $.
+    rspcime.2 $e |- ( ph -> A e. B ) $.
+    $( Prove a restricted existential.  (Contributed by Rohan Ridenour,
+       3-Aug-2023.) $)
+    rspcime $p |- ( ph -> E. x e. B ps ) $=
+      ( cv wceq wa simpl 2thd id rspcedvd ) ABACDEGACHDIZJBAFAOKLAMN $.
+  $}
+
   ${
     $d x y A $.  $d x B $.  $d x C $.  $d x ps $.  $d x ch $.
     rspceaimv.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
@@ -42746,6 +42763,29 @@ is most interesting when the natural number is a successor (as seen in
       NRABGOABCDEHFPQ $.
   $}
 
+  ${
+    $d D x $.  $d x A $.  $d x C $.  $d x ph $.
+    elrnmptdv.1 $e |- F = ( x e. A |-> B ) $.
+    elrnmptdv.2 $e |- ( ph -> C e. A ) $.
+    elrnmptdv.3 $e |- ( ph -> D e. V ) $.
+    elrnmptdv.4 $e |- ( ( ph /\ x = C ) -> D = B ) $.
+    $( Elementhood in the range of a function in maps-to notation, deduction
+       form.  (Contributed by Rohan Ridenour, 3-Aug-2023.) $)
+    elrnmptdv $p |- ( ph -> D e. ran F ) $=
+      ( crn wcel wceq wrex rspcime wb elrnmpt syl mpbird ) AFGMNZFDOZBCPZAUCBEC
+      LJQAFHNUBUDRKBCDFGHISTUA $.
+  $}
+
+  ${
+    $d x C $.
+    elrnmpt2d.1 $e |- F = ( x e. A |-> B ) $.
+    elrnmpt2d.2 $e |- ( ph -> C e. ran F ) $.
+    $( Elementhood in the range of a function in maps-to notation, deduction
+       form.  (Contributed by Rohan Ridenour, 3-Aug-2023.) $)
+    elrnmpt2d $p |- ( ph -> E. x e. A C = B ) $=
+      ( crn wcel wceq wrex elrnmpt ibi syl ) AEFIZJZEDKBCLZHQRBCDEFPGMNO $.
+  $}
+
   $( The range of the empty set is empty.  Part of Theorem 3.8(v) of [Monk1]
      p. 36.  (Contributed by NM, 4-Jul-1994.) $)
   rn0 $p |- ran (/) = (/) $=
@@ -64120,6 +64160,20 @@ the first case of his notation (simple exponentiation) and subscript it
       UEUFUGUHUIUJUK $.
   $}
 
+  ${
+    enpr2d.1 $e |- ( ph -> A e. C ) $.
+    enpr2d.2 $e |- ( ph -> B e. D ) $.
+    enpr2d.3 $e |- ( ph -> -. A = B ) $.
+    $( A pair with distinct elements is equinumerous to ordinal two.
+       (Contributed by Rohan Ridenour, 3-Aug-2023.) $)
+    enpr2d $p |- ( ph -> { A , B } ~~ 2o ) $=
+      ( c1o cen csn cun wbr cin c0 wceq wcel syl con0 1on cpr csuc ensn1g en2sn
+      c2o sylancl wne neqned disjsn2 wn onirri a1i disjsn sylibr syl22anc df-pr
+      unen df-suc 3brtr4g df-2o breqtrrdi ) ABCUAZIUBZUEJABKZCKZLZIIKZLZVBVCJAV
+      DIJMZVEVGJMZVDVENOPZIVGNOPZVFVHJMABDQVIFBDUCRACEQISQVJGTCIESUDUFABCUGVKAB
+      CHUHBCUIRAIIQUJZVLVMAITUKULIIUMUNVDIVEVGUQUOBCUPIURUSUTVA $.
+  $}
+
   $( A subset of a set dominated by ` _om ` is dominated by ` _om ` .
      (Contributed by Thierry Arnoux, 31-Jan-2017.) $)
   ssct $p |- ( ( A C_ B /\ B ~<_ _om ) -> A ~<_ _om ) $=
@@ -66084,6 +66138,18 @@ texts assume excluded middle (in which case the two intersection
       XA $.
   $}
 
+  ${
+    phpeqd.1 $e |- ( ph -> A e. Fin ) $.
+    phpeqd.2 $e |- ( ph -> B C_ A ) $.
+    phpeqd.3 $e |- ( ph -> A ~~ B ) $.
+    $( Corollary of the Pigeonhole Principle using equality.  Strengthening of
+       ~ phpm expressed without negation.  (Contributed by Rohan Ridenour,
+       3-Aug-2023.) $)
+    phpeqd $p |- ( ph -> A = B ) $=
+      ( cfn wcel wss cen wbr wceq w3a ensymb fisseneq syl3an3br eqcomd syl3anc
+      ) ABGHZCBIZBCJKZBCLDEFSTUAMCBUASTCBJKCBLCBNCBOPQR $.
+  $}
+
   ${
     $d A w x y z $.  $d ph w y z $.  $d ps w y z $.
     ssfirab.a $e |- ( ph -> A e. Fin ) $.
@@ -125102,6 +125168,31 @@ which defines the set we are taking the supremum of must (a) be true at
     ( cz wcel c1 cgcd co wceq 1z gcdcom mpan gcd1 eqtrd ) ABCZDAEFZADEFZDDBCMNO
     GHDAIJAKL $.
 
+  ${
+    gcdmultipled.1 $e |- ( ph -> M e. NN0 ) $.
+    gcdmultipled.2 $e |- ( ph -> N e. ZZ ) $.
+    $( The greatest common divisor of a nonnegative integer ` M ` and a
+       multiple of it is ` M ` itself.  (Contributed by Rohan Ridenour,
+       3-Aug-2023.) $)
+    gcdmultipled $p |- ( ph -> ( M gcd ( N x. M ) ) = M ) $=
+      ( cc0 cgcd co cmul caddc cz wcel wceq nn0zd 0zd gcdaddm syl3anc nn0gcdid0
+      cn0 syl zmulcld zcnd addid2d oveq2d 3eqtr3rd ) ABFGHZBFCBIHZJHZGHZBBUGGHA
+      CKLBKLFKLUFUIMEABDNZAOCBFPQABSLUFBMDBRTAUHUGBGAUGAUGACBEUJUAUBUCUDUE $.
+  $}
+
+  ${
+    dvdsgcdidd.1 $e |- ( ph -> M e. NN ) $.
+    dvdsgcdidd.2 $e |- ( ph -> N e. ZZ ) $.
+    dvdsgcdidd.3 $e |- ( ph -> M || N ) $.
+    $( The greatest common divisor of a positive integer and another integer it
+       divides is itself.  (Contributed by Rohan Ridenour, 3-Aug-2023.) $)
+    dvdsgcdidd $p |- ( ph -> ( M gcd N ) = M ) $=
+      ( cdiv co cmul cgcd zcnd nncnd nnap0d divcanap1d oveq2d nnnn0d cdvds wcel
+      wbr cz cc0 wne wb nnzd nnne0d dvdsval2 syl3anc mpbid gcdmultipled eqtr3d
+      ) ABCBGHZBIHZJHBCJHBAULCBJACBACEKABDLABDMNOABUKABDPABCQSZUKTRZFABTRBUAUBC
+      TRUMUNUCABDUDABDUEEBCUFUGUHUIUJ $.
+  $}
+
   $( The greatest common divisor of six and four is two.  To calculate this
      gcd, a simple form of Euclid's algorithm is used:
      ` ( 6 gcd 4 ) = ( ( 4 + 2 ) gcd 4 ) = ( 2 gcd 4 ) ` and

diff --git a/mmil.raw.html b/mmil.raw.html
@@ -8072,11 +8072,23 @@
   <TD>~ fihashneq0</TD>
 </TR>
 
+<tr>
+  <td>hashelne0d</td>
+  <td><i>none</i></td>
+  <td>would be easy to prove if ` A e. V ` is changed to ` A e. Fin `</td>
+</tr>
+
 <TR>
   <TD>hashen1</TD>
   <TD>~ fihashen1</TD>
 </TR>
 
+<tr>
+  <td>hash1elsn</td>
+  <td><i>none</i></td>
+  <td>would be easy to prove if ` A e. V ` is changed to ` A e. Fin `</td>
+</tr>
+
 <TR>
   <TD>hashrabrsn</TD>
   <TD><I>none</I></TD>
@@ -8366,6 +8378,12 @@
   to ` _om ~<_ A ` but the set.mm proof does not work as is.</TD>
 </TR>
 
+<tr>
+  <td>phphashd , phphashrd</td>
+  <td><i>none</i></td>
+  <td>would appear to need hashclb or some other way of showing that
+  the subset is finite</td>
+</tr>
 
 <TR>
   <TD>seqcoll</TD>