fix definition bugs (#3247)

* fix definition bugs

* actually a bug in the definition checker

* wcel2-wl isn't primitive

* Remove typesetting definition for wl-in

---------

Co-authored-by: Thierry Arnoux <[email protected]>

discouraged

@@ -14743,7 +14743,6 @@ New usage of "conventions" is discouraged (0 uses).
 New usage of "conventions-comments" is discouraged (0 uses).
 New usage of "conventions-labels" is discouraged (0 uses).
 New usage of "counop" is discouraged (0 uses).
-New usage of "cqpOLD" is discouraged (0 uses).
 New usage of "crhmsubcALTV" is discouraged (1 uses).
 New usage of "cringcALTV" is discouraged (9 uses).
 New usage of "cringcatALTV" is discouraged (0 uses).
@@ -18194,17 +18193,8 @@ New usage of "wrdsplexOLD" is discouraged (0 uses).
 New usage of "wrdvOLD" is discouraged (0 uses).
 New usage of "wvd2" is discouraged (5 uses).
 New usage of "wvd3" is discouraged (3 uses).
-New usage of "wvhc10" is discouraged (0 uses).
-New usage of "wvhc11" is discouraged (0 uses).
-New usage of "wvhc12" is discouraged (0 uses).
 New usage of "wvhc2" is discouraged (5 uses).
 New usage of "wvhc3" is discouraged (3 uses).
-New usage of "wvhc4" is discouraged (0 uses).
-New usage of "wvhc5" is discouraged (0 uses).
-New usage of "wvhc6" is discouraged (0 uses).
-New usage of "wvhc7" is discouraged (0 uses).
-New usage of "wvhc8" is discouraged (0 uses).
-New usage of "wvhc9" is discouraged (0 uses).
 New usage of "wwlksm1edgOLD" is discouraged (1 uses).
 New usage of "wwlksnextbiOLD" is discouraged (0 uses).
 New usage of "wwlksnextbij0OLD" is discouraged (1 uses).

set.mm

@@ -11715,6 +11715,9 @@ When the universe is infinite (as with set theory), such a
     wal $a wff A. x ph $.
   $}
 
+  $( Register 'A.' as a primitive expression (lacking a definition). $)
+  $( $j primitive 'wal'; $)
+
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
@@ -11798,6 +11801,10 @@ When the universe is infinite (as with set theory), such a
     wceq $a wff A = B $.
   $}
 
+  $( Register class-to-set promotion and class equality as primitive
+     expressions. $)
+  $( $j primitive 'cv' 'wceq'; $)
+
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
@@ -14311,9 +14318,6 @@ introduce universal quantification ("for all", e.g. ~ ax-4 ) in order to
   $( Let ` t ` be an individual variable. $)
   vt $f setvar t $.
 
-  $( Register 'A.' as a primitive expression (lacking a definition). $)
-  $( $j primitive 'wal'; $)
-
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
@@ -17212,6 +17216,9 @@ disjoint variable condition ( ~ sb2 ).  Theorem ~ sb6f replaces the
     wcel $a wff A e. B $.
   $}
 
+  $( Register class membership as a primitive expression. $)
+  $( $j primitive 'wcel'; $)
+
   $( Extend wff definition to include atomic formulas with the membership
      predicate.  This is read " ` x ` is an element of ` y ` ", " ` x ` is a
      member of ` y ` ", " ` x ` belongs to ` y ` ", or " ` y ` contains
@@ -17243,12 +17250,6 @@ disjoint variable condition ( ~ sb2 ).  Theorem ~ sb6f replaces the
   wel $p wff x e. y $=
     ( cv wcel ) ACBCD $.
 
-  $( Register class-to-set promotion and class equality and membership as
-     primitive expressions. Although these are actually definitions, the above
-     ambiguity prevention necessitates our taking class equality as the
-     primitive, instead of set equality. $)
-  $( $j primitive 'weq' 'wel'; $)
-
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -24608,7 +24609,7 @@ range over class builders (implicitly in the case of defined class terms
      variables to class variables via the use of ~ cv . $)
   cab $a class { x | ph } $.
 
-  $( $j primitive 'cv' 'wceq' 'wcel' 'cab'; $)
+  $( $j primitive 'cab'; $)
 
   $( Let ` A ` be a class variable. $)
   cA $f class A $.
@@ -437920,8 +437921,6 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
   latexdef "/Qp" as "/_{\mathbb{Q}_p}";
 htmldef "Qp" as "Qp"; althtmldef "Qp" as "Qp";
   latexdef "Qp" as "\mathbb{Q}_p";
-htmldef "QpOLD" as "QpOLD"; althtmldef "QpOLD" as "QpOLD";
-  latexdef "QpOLD" as "\mathbb{Q}_p";
 htmldef "Zp" as "Zp"; althtmldef "Zp" as "Zp";
   latexdef "Zp" as "\mathbb{Z}_p";
 htmldef "_Qp" as "_Qp"; althtmldef "_Qp" as "_Qp";
@@ -507465,7 +507464,7 @@ valuation of the variables (v_0 ` = ( S `` (/) ) ` , v_1 ` = ( S `` 1o
   df-m0s $a |- m0St = ( a e. _V |-> <. (/) , (/) , a >. ) $.
 
   ${
-    $d a d e h m o p r s t x y $.
+    $d a c d e h m o p r s t x y $.
     $( Define the set of syntax axioms.  (Contributed by Mario Carneiro,
        14-Jul-2016.) $)
     df-msa $a |- mSA = ( t e. _V |-> { a e. ( mEx ` t ) |
@@ -507482,6 +507481,21 @@ valuation of the variables (v_0 ` = ( S `` (/) ) ` , v_1 ` = ( S `` 1o
        14-Jul-2016.) $)
     df-msyn $a |- mSyn = Slot 6 $.
 
+    $( Define the syntax typecode function for expressions.  (Contributed by
+       Mario Carneiro, 12-Jun-2023.) $)
+    df-mesyn $a |- mESyn = ( t e. _V |->
+      ( c e. ( mTC ` t ) , e e. ( mREx ` t ) |->
+        ( ( ( mSyn ` t ) ` c ) m0St e ) ) ) $.
+
+    $( Define the set of grammatical formal systems.  (Contributed by Mario
+       Carneiro, 12-Jun-2023.) $)
+    df-mgfs $a |- mGFS = { t e. mWGFS |
+      ( ( mSyn ` t ) : ( mTC ` t ) --> ( mVT ` t ) /\
+        A. c e. ( mVT ` t ) ( ( mSyn ` t ) ` c ) = c /\
+        A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) ->
+          A. e e. ( h u. { a } )
+            ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) ) ) } $.
+
     $( Define the set of proof trees.  (Contributed by Mario Carneiro,
        14-Jul-2016.) $)
     df-mtree $a |- mTree = ( t e. _V |->
@@ -507833,7 +507847,7 @@ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\
   $c GF_oo $. $( Galois limit field $)
   $c ~Qp $. $( Equivalence relation for Qp $)
   $c /Qp $. $( Representative of equivalence relation $)
-  $c Qp QpOLD $. $( p-adic rational numbers $)
+  $c Qp $. $( p-adic rational numbers $)
   $c Zp $. $( p-adic integers $)
   $c _Qp $. $( Algebraic completion of Qp $)
   $c Cp $. $( Metric completion of _Qp $)
@@ -507856,9 +507870,6 @@ h C_ ( dom n " { m } ) ) -> m dom n a ) ) ) /\
   $( The set of ` p ` -adic rational numbers. $)
   cqp $a class Qp $.
 
-  $( The set of ` p ` -adic rational numbers.  (New usage is discouraged.) $)
-  cqpOLD $a class QpOLD $.
-
   $( The set of ` p ` -adic integers.  (Not to be confused with ~ czn .) $)
   czp $a class Zp $.
 
@@ -525045,6 +525056,9 @@ theory containing Robinson arithmetic (a fragment of Peano arithmetic), one
   $( Syntax for the provability predicate. $)
   cprvb $a wff Prv ph $.
 
+  $( We take 'Prv ph' as a primitive expression (lacking a definition). $)
+  $( $j primitive 'cprvb'; $)
+
   ${
     ax-prv1.1 $e |- ph $.
     $( First property of three of the provability predicate.  (Contributed by
@@ -651620,45 +651634,6 @@ Why not create a separate database (setg.mm) of proofs in G1, avoiding
       ( wvhc3 wvd1 w3a wi dfvd3an mpbir ) ABCFDGABCHDIEABCDJK $.
   $}
 
-  $( Syntax for a 4-element virtual hypotheses collection.  (Contributed by
-     Alan Sare, 17-Oct-2017.)  (New usage is discouraged.) $)
-  wvhc4 $a wff (. ph ,. ps ,. ch ,. th ). $.
-
-  $( Syntax for a 5-element virtual hypotheses collection.  (Contributed by
-     Alan Sare, 17-Oct-2017.)  (New usage is discouraged.) $)
-  wvhc5 $a wff (. ph ,. ps ,. ch ,. th ,. ta ). $.
-
-  $( Syntax for a 6-element virtual hypotheses collection.  (Contributed by
-     Alan Sare, 17-Oct-2017.)  (New usage is discouraged.) $)
-  wvhc6 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ). $.
-
-  $( Syntax for a 7-element virtual hypotheses collection.  (Contributed by
-     Alan Sare, 17-Oct-2017.)  (New usage is discouraged.) $)
-  wvhc7 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ). $.
-
-  $( Syntax for an 8-element virtual hypotheses collection.  (Contributed by
-     Alan Sare, 17-Oct-2017.)  (New usage is discouraged.) $)
-  wvhc8 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ). $.
-
-  $( Syntax for a 9-element virtual hypotheses collection.  (Contributed by
-     Alan Sare, 17-Oct-2017.)  (New usage is discouraged.) $)
-  wvhc9 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ). $.
-
-  $( Syntax for a 10-element virtual hypotheses collection.  (Contributed by
-     Alan Sare, 17-Oct-2017.)  (New usage is discouraged.) $)
-  wvhc10 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,.
-                   ze ,. si ,. rh ,. mu ). $.
-
-  $( Syntax for an 11-element virtual hypotheses collection.  (Contributed by
-     Alan Sare, 17-Oct-2017.)  (New usage is discouraged.) $)
-  wvhc11 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,.
-                   ze ,. si ,. rh ,. mu ,. la ). $.
-
-  $( Syntax for a 12-element virtual hypotheses collection.  (Contributed by
-     Alan Sare, 17-Oct-2017.)  (New usage is discouraged.) $)
-  wvhc12 $a wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,.
-                   ze ,. si ,. rh ,. mu ,. la ,. ka ). $.
-
   ${
     vd01.1 $e |- ph $.
     $( A virtual hypothesis virtually infers a theorem.  (Contributed by Alan