Add norass in parallel with existing nanass. (#3601)

Shorten Richard Penner to RP in my mathbox.

Author: arpie-steele

set.mm

@@ -11688,6 +11688,22 @@ This definition (in the form of ~ dfifp2 ) appears in Section II.24 of
     ( wnor wo wn notnotb df-nor notbii nornot 3bitr2ri bicomi ) ABCZLCZABDZNNEZ
     ELEMNFLOABGHLIJK $.
 
+  $( A characterization of when an expression involving nor associates.  This
+     is identical to the case when alternative denial is associative, see
+     ~ nanass .  Remark:  Like alternative denial, nor is also commutative, see
+     ~ norcom .  (Contributed by RP, 29-Oct-2023.) $)
+  norass $p |- ( ( ph <-> ch ) <->
+                 ( ( ( ph -\/ ps ) -\/ ch ) <-> ( ph -\/ ( ps -\/ ch ) ) ) ) $=
+    ( wb wn wa wnor notbid wi wo olc oran sylib anim1ci animorl ex df-nor ioran
+    jcn 3bitri id bicomd anbi2d anbi12d con4d com12 anim12i dfbi2 impbii norcom
+    3imtr4i notbii anbi2i bitri bibi12i bitr4i ) ACDZCEZBEZAEZFZEZFZUTUSURFZEZF
+    ZDZABGZCGZABCGZGZDUQVGUQURUTVBVEUQUTURUQACUQUAHZUBUQVAVDUQUTURUSVLUCHUDVCVF
+    IZVFVCIZFACIZCAIZFVGUQVMVOVNVPAVMCACVMAURVMEAURFZVCVFAVBURABAJZVBABKBALMNVQ
+    AVDJVFEAURVDOAVDLMSPUEUFCVNACAVNCUTVNECUTFZVFVCCVEUTCBCJZVECBKBCLMNVSCVAJVC
+    ECUTVAOCVALMSPUEUFUGVCVFUHACUHUKUIVIVCVKVFVICVHGCVHJEZVCVHCUJCVHQWAURVHEZFV
+    CCVHRWBVBURVHVAVHBAGVREVAABUJBAQBARTULUMUNTVKAVJJEUTVJEZFVFAVJQAVJRWCVEUTVJ
+    VDVJVTEVDBCQBCRUNULUMTUOUP $.
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   True and false constants
@@ -635983,7 +635999,7 @@ is in the span of P(i)(X), so there is an R-linear combination of
 $)
 
   $( A special case where implication appears to conform to a mixed associative
-     law.  (Contributed by Richard Penner, 29-Feb-2020.) $)
+     law.  (Contributed by RP, 29-Feb-2020.) $)
   rp-fakeimass $p |- ( ( ph \/ ch ) <->
                        ( ( ( ph -> ps ) -> ch )
                          <-> ( ph -> ( ps -> ch ) ) ) ) $=
@@ -635993,7 +636009,7 @@ is in the span of P(i)(X), so there is an R-linear combination of
     EEUGGUMACAUHTUAUBUCUD $.
 
   $( A special case where a mixture of and and or appears to conform to a mixed
-     associative law.  (Contributed by Richard Penner, 26-Feb-2020.) $)
+     associative law.  (Contributed by RP, 26-Feb-2020.) $)
   rp-fakeanorass $p |- ( ( ch -> ph ) <->
                          ( ( ( ph /\ ps ) \/ ch )
                            <-> ( ph /\ ( ps \/ ch ) ) ) ) $=
@@ -636004,7 +636020,7 @@ is in the span of P(i)(X), so there is an R-linear combination of
     RUMABCUFUGUHUI $.
 
   $( A special case where a mixture of or and and appears to conform to a mixed
-     associative law.  (Contributed by Richard Penner, 29-Feb-2020.) $)
+     associative law.  (Contributed by RP, 29-Feb-2020.) $)
   rp-fakeoranass $p |- ( ( ph -> ch ) <->
                          ( ( ( ph \/ ps ) /\ ch )
                            <-> ( ph \/ ( ps /\ ch ) ) ) ) $=
@@ -636015,7 +636031,7 @@ is in the span of P(i)(X), so there is an R-linear combination of
   ${
     $d x A $.  $d x B $.  $d x C $.
     $( A special case where a mixture of intersection and union appears to
-       conform to a mixed associative law.  (Contributed by Richard Penner,
+       conform to a mixed associative law.  (Contributed by RP,
        26-Feb-2020.) $)
     rp-fakeinunass $p |- ( C C_ A <->
                            ( ( A i^i B ) u. C ) = ( A i^i ( B u. C ) ) ) $=
@@ -636027,8 +636043,7 @@ is in the span of P(i)(X), so there is an R-linear combination of
   $}
 
   $( A special case where a mixture of union and intersection appears to
-     conform to a mixed associative law.  (Contributed by Richard Penner,
-     29-Feb-2020.) $)
+     conform to a mixed associative law.  (Contributed by RP, 29-Feb-2020.) $)
   rp-fakeuninass $p |- ( A C_ C <->
                          ( ( A u. B ) i^i C ) = ( A u. ( B i^i C ) ) ) $=
     ( wss cin wceq rp-fakeinunass eqcom incom uncom ineq1i eqtri uneq2i eqeq12i
@@ -636049,7 +636064,7 @@ is in the span of P(i)(X), so there is an R-linear combination of
     $d n A $.
     $( A set is said to be finite if it can be put in one-to-one correspondence
        with all the natural numbers between 1 and some ` n e. NN0 ` .
-       (Contributed by Richard Penner, 3-Mar-2020.) $)
+       (Contributed by RP, 3-Mar-2020.) $)
     rp-isfinite5 $p |- ( A e. Fin <-> E. n e. NN0 ( 1 ... n ) ~~ A ) $=
       ( cfn wcel c1 cv cfz co cen wbr cn0 wrex chash cfv cvv oveq2 mpsyl sylibr
       wa wceq wex fvex hashcl isfinite4 biimpi jca breq1d anbi12d spcegv df-rex
@@ -636065,7 +636080,7 @@ is in the span of P(i)(X), so there is an R-linear combination of
     $d n A $.
     $( A set is said to be finite if it is either empty or it can be put in
        one-to-one correspondence with all the natural numbers between 1 and
-       some ` n e. NN ` .  (Contributed by Richard Penner, 10-Mar-2020.) $)
+       some ` n e. NN ` .  (Contributed by RP, 10-Mar-2020.) $)
     rp-isfinite6 $p |- ( A e. Fin <-> ( A = (/) \/
                                         E. n e. NN ( 1 ... n ) ~~ A ) ) $=
       ( cfn wcel c0 wceq wa wn wo c1 cfz cen wbr cn bitri cn0 wex w3a cc0 syl
@@ -636171,7 +636186,7 @@ of all sets ( ~ inex1g ).
     $d u v x y A $.
     $( A definition of the finite intersection property of a class based on
        closure under pairwise intersection of its elements is independent of
-       the dummy variables.  (Contributed by Richard Penner, 1-Jan-2020.) $)
+       the dummy variables.  (Contributed by RP, 1-Jan-2020.) $)
     fipjust $p |- ( A. u e. A A. v e. A ( u i^i v ) e. A
                     <-> A. x e. A A. y e. A ( x i^i y ) e. A ) $=
       ( cv cin wcel weq ineq1 eleq1d ineq2 cbvral2v ) DFZCFZGZEHAFZBFZGZEHQOGZE
@@ -636188,7 +636203,7 @@ of all sets ( ~ inex1g ).
     cllem0.closed $e |- ( ( ch /\ th ) -> ps ) $.
     $( The class of all sets with property ` ph ( z ) ` is closed under the
        binary operation on sets defined in ` R ( x , y ) ` .  (Contributed by
-       Richard Penner, 3-Jan-2020.) $)
+       RP, 3-Jan-2020.) $)
     cllem0 $p |- A. x e. V A. y e. V R e. V $=
       ( wcel wral elab2 ralbii cv wi wal elexi df-ral 3bitri syl2anb ex alrimiv
       vex mpgbir ) HJQZFJRZEJRZEUAZJQZFUAZJQZBUBZFUCZUBZEUNBFJRZEJRUTEJRVAEUCUM
@@ -636200,14 +636215,14 @@ of all sets ( ~ inex1g ).
     $d x y z $.  $d y A $.  $d z B $.
     superficl.a $e |- A = { z | B C_ z } $.
     $( The class of all supersets of a class has the finite intersection
-       property.  (Contributed by Richard Penner, 1-Jan-2020.)  (Proof
-       shortened by Richard Penner, 3-Jan-2020.) $)
+       property.  (Contributed by RP, 1-Jan-2020.)  (Proof shortened by RP,
+       3-Jan-2020.) $)
     superficl $p |- A. x e. A A. y e. A ( x i^i y ) e. A $=
       ( cv wss cin cvv vex inex1 sseq2 wa ssin biimpi cllem0 ) ECGZHEAGZBGZIZHZ
       ESHZETHZABCUAJDFSTAKLRUAEMRSEMRTEMUCUDNUBESTOPQ $.
 
     $( The class of all supersets of a class is closed under binary union.
-       (Contributed by Richard Penner, 3-Jan-2020.) $)
+       (Contributed by RP, 3-Jan-2020.) $)
     superuncl $p |- A. x e. A A. y e. A ( x u. y ) e. A $=
       ( cv wss cun cvv vex unex sseq2 ssun3 adantr cllem0 ) ECGZHEAGZBGZIZHZERH
       ZESHZABCTJDFRSAKBKLQTEMQREMQSEMUBUAUCERSNOP $.
@@ -636218,26 +636233,26 @@ of all sets ( ~ inex1g ).
     $( N.B. This hypothesis is same as the power class of B. $)
     ssficl.a $e |- A = { z | z C_ B } $.
     $( The class of all subsets of a class has the finite intersection
-       property.  (Contributed by Richard Penner, 1-Jan-2020.)  (Proof
-       shortened by Richard Penner, 3-Jan-2020.) $)
+       property.  (Contributed by RP, 1-Jan-2020.)  (Proof shortened by RP,
+       3-Jan-2020.) $)
     ssficl $p |- A. x e. A A. y e. A ( x i^i y ) e. A $=
       ( cv wss cin cvv vex inex1 sseq1 ssinss1 adantr cllem0 ) CGZEHAGZBGZIZEHZ
       REHZSEHZABCTJDFRSAKLQTEMQREMQSEMUBUAUCRSENOP $.
 
     $( The class of all subsets of a class is closed under binary union.
-       (Contributed by Richard Penner, 3-Jan-2020.) $)
+       (Contributed by RP, 3-Jan-2020.) $)
     ssuncl $p |- A. x e. A A. y e. A ( x u. y ) e. A $=
       ( cv wss cun cvv vex unex sseq1 wa unss biimpi cllem0 ) CGZEHAGZBGZIZEHZS
       EHZTEHZABCUAJDFSTAKBKLRUAEMRSEMRTEMUCUDNUBSTEOPQ $.
 
     $( The class of all subsets of a class is closed under class difference.
-       (Contributed by Richard Penner, 3-Jan-2020.) $)
+       (Contributed by RP, 3-Jan-2020.) $)
     ssdifcl $p |- A. x e. A A. y e. A ( x \ y ) e. A $=
       ( cv wss cdif cvv vex difexi sseq1 ssdifss adantr cllem0 ) CGZEHAGZBGZIZE
       HZREHZSEHZABCTJDFRSAKLQTEMQREMQSEMUBUAUCRESNOP $.
 
     $( The class of all subsets of a class is closed under symmetric
-       difference.  (Contributed by Richard Penner, 3-Jan-2020.) $)
+       difference.  (Contributed by RP, 3-Jan-2020.) $)
     sssymdifcl $p |- A. x e. A A. y e. A ( ( x \ y ) u. ( y \ x ) ) e. A $=
       ( cv wss cdif cun cvv wcel vex difexg ax-mp unex sseq1 ssdifss wa unss
       biimpi syl2an cllem0 ) CGZEHAGZBGZIZUFUEIZJZEHZUEEHZUFEHZABCUIKDFUGUHUEKL
@@ -636251,7 +636266,7 @@ of all sets ( ~ inex1g ).
     fiinfi.b $e |- ( ph -> A. x e. B A. y e. B ( x i^i y ) e. B ) $.
     fiinfi.c $e |- ( ph -> C = ( A i^i B ) ) $.
     $( If two classes have the finite intersection property, then so does their
-       intersection.  (Contributed by Richard Penner, 1-Jan-2020.) $)
+       intersection.  (Contributed by RP, 1-Jan-2020.) $)
     fiinfi $p |- ( ph -> A. x e. C A. y e. C ( x i^i y ) e. C ) $=
       ( cv cin wcel wral elinel1 imim1i ralimi2 imim12i syl ralbidv mpbird elin
       wa elinel2 r19.26-2 sylanbrc 2ralbii sylibr eleq2d raleqdv ) ABJZCJZKZFLZ
@@ -637468,13 +637483,13 @@ of all sets ( ~ inex1g ).
   ${
     conrel1d.a $e |- ( ph -> `' A = (/) ) $.
     $( Deduction about composition with a class with no relational content.
-       (Contributed by Richard Penner, 24-Dec-2019.) $)
+       (Contributed by RP, 24-Dec-2019.) $)
     conrel1d $p |- ( ph -> ( A o. B ) = (/) ) $=
       ( cdm crn cin incom wceq ccnv dfdm4 rneqd rn0 syl6eq syl5eq ineq2 in0 syl
       c0 coemptyd ) ABCABEZCFZGUBUAGZSUAUBHAUASIZUCSIAUABJZFZSBKAUFSFSAUESDLMNO
       UDUCUBSGSUASUBPUBQNROT $.
     $( Deduction about composition with a class with no relational content.
-       (Contributed by Richard Penner, 24-Dec-2019.) $)
+       (Contributed by RP, 24-Dec-2019.) $)
     conrel2d $p |- ( ph -> ( B o. A ) = (/) ) $=
       ( cdm crn cin ccnv c0 wceq df-rn ineq2i a1i dmeqd ineq2d dm0 eqtri 3eqtrd
       in0 coemptyd ) ACBACEZBFZGZUABHZEZGZUAIEZGZIUCUFJAUBUEUABKLMAUEUGUAAUDIDN
@@ -637493,7 +637508,7 @@ Transitive relations (not to be confused with transitive classes).
     trrelind.s $e |- ( ph -> ( S o. S ) C_ S ) $.
     trrelind.t $e |- ( ph -> T = ( R i^i S ) ) $.
     $( The intersection of transitive relations is a transitive relation.
-       (Contributed by Richard Penner, 24-Dec-2019.) $)
+       (Contributed by RP, 24-Dec-2019.) $)
     trrelind $p |- ( ph -> ( T o. T ) C_ T ) $=
       ( cin ccom wss inss1 a1i trrelssd inss2 ssind coeq12d 3sstr4d ) ABCHZRIZR
       DDIDASBCABRRERBJABCKLZTMACRRFRCJABCNLZUAMOADRDRGGPGQ $.
@@ -637503,7 +637518,7 @@ Transitive relations (not to be confused with transitive classes).
     xpintrreld.r $e |- ( ph -> ( R o. R ) C_ R ) $.
     xpintrreld.s $e |- ( ph -> S = ( R i^i ( A X. B ) ) ) $.
     $( The intersection of a transitive relation with a cross product is a
-       transitve relation.  (Contributed by Richard Penner, 24-Dec-2019.) $)
+       transitve relation.  (Contributed by RP, 24-Dec-2019.) $)
     xpintrreld $p |- ( ph -> ( S o. S ) C_ S ) $=
       ( cxp ccom wss xptrrel a1i trrelind ) ADBCHZEFNNINJABCKLGM $.
   $}
@@ -637512,7 +637527,7 @@ Transitive relations (not to be confused with transitive classes).
     restrreld.r $e |- ( ph -> ( R o. R ) C_ R ) $.
     restrreld.s $e |- ( ph -> S = ( R |` A ) ) $.
     $( The restriction of a transitive relation is a transitive relation.
-       (Contributed by Richard Penner, 24-Dec-2019.) $)
+       (Contributed by RP, 24-Dec-2019.) $)
     restrreld $p |- ( ph -> ( S o. S ) C_ S ) $=
       ( cvv cres cxp cin df-res syl6eq xpintrreld ) ABGCDEADCBHCBGIJFCBKLM $.
   $}
@@ -637521,7 +637536,7 @@ Transitive relations (not to be confused with transitive classes).
     trrelsuperreldg.r $e |- ( ph -> Rel R ) $.
     trrelsuperreldg.s $e |- ( ph -> S = ( dom R X. ran R ) ) $.
     $( Concrete construction of a superclass of relation ` R ` which is a
-       transitive relation.  (Contributed by Richard Penner, 25-Dec-2019.) $)
+       transitive relation.  (Contributed by RP, 25-Dec-2019.) $)
     trrelsuperreldg $p |- ( ph -> ( R C_ S /\ ( S o. S ) C_ S ) ) $=
       ( wss ccom cdm crn cxp relssdmrn syl sseqtr4d xptrrel a1i coeq12d 3sstr4d
       wrel jca ) ABCFCCGZCFABBHZBIZJZCABRBUCFDBKLEMAUCUCGZUCTCUDUCFAUAUBNOACUCC
@@ -637532,8 +637547,8 @@ Transitive relations (not to be confused with transitive classes).
     $d x y z $.  $d y A $.
     trficl.a $e |- A = { z | ( z o. z ) C_ z } $.
     $( The class of all transitive relations has the finite intersection
-       property.  (Contributed by Richard Penner, 1-Jan-2020.)  (Proof
-       shortened by Richard Penner, 3-Jan-2020.) $)
+       property.  (Contributed by RP, 1-Jan-2020.)  (Proof shortened by RP,
+       3-Jan-2020.) $)
     trficl $p |- A. x e. A A. y e. A ( x i^i y ) e. A $=
       ( cv ccom wss cin cvv vex inex1 wceq id coeq12d sseq12d weq trin2 cllem0
       ) CFZTGZTHAFZBFZIZUDGZUDHUBUBGZUBHUCUCGZUCHABCUDJDEUBUCAKLTUDMZUAUETUDUHT
@@ -637542,7 +637557,7 @@ Transitive relations (not to be confused with transitive classes).
   $}
 
   $( The converse of a transitive relation is a transitive relation.
-     (Contributed by Richard Penner, 25-Dec-2019.) $)
+     (Contributed by RP, 25-Dec-2019.) $)
   cnvtrrel $p |- ( ( S o. S ) C_ S <-> ( `' S o. `' S ) C_ `' S ) $=
     ( ccom wss ccnv cnvss cnvco cnveqi cocnvcnv1 cocnvcnv2 3eqtri sseq1i biimpi
     eqtri cnvcnvss syl6ss syl impbii bitri ) AABZACZSDZADZCZUBUBBZUBCTUCSAEUCUA
@@ -639550,7 +639565,7 @@ adopting f( ` ph ` ) as ` if- ( ph , ps , ch ) ` would result in the
 
   $( If the ` R ` -image of a class ` A ` is a subclass of ` B ` , then the
      restriction of ` R ` to ` A ` is a subset of the Cartesian product of
-     ` A ` and ` B ` .  (Contributed by Richard Penner, 24-Dec-2019.) $)
+     ` A ` and ` B ` .  (Contributed by RP, 24-Dec-2019.) $)
   rp-imass $p |- ( ( R " A ) C_ B <-> ( R |` A ) C_ ( A X. B ) ) $=
     ( cima wss cres crn cdm cxp df-ima sseq1i dmres inss1 eqsstri biantrur wrel
     wa cin relres syl6ss relssdmrn xpss12 syl5ss dmss dmxpss rnss rnxpss impbii