dfantisymrel4, antisymrelressn

mazsa · Jan 3, 2025 · 4a97e01 · 4a97e01
1 parent b888ff2
commit 4a97e01
Showing 1 changed file with 138 additions and 0 deletions.
diff --git a/set.mm b/set.mm
@@ -450831,6 +450831,9 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
 htmldef "ElDisj" as ' ElDisj ';
   althtmldef "ElDisj" as ' ElDisj ';
   latexdef "ElDisj" as "\mathrm{ElDisj}";
+htmldef "AntisymRel" as ' AntisymRel ';
+  althtmldef "AntisymRel" as ' AntisymRel ';
+  latexdef "AntisymRel" as "\mathrm{AntisymRel}";
 /* End of Peter Mazsa's mathbox */
 
 /* Mathbox of Rodolfo Medina */
@@ -580791,6 +580794,8 @@ A collection of theorems for commuting equalities (or
                    relation $)
   $c ElDisj $. $( Disjoint elementhood predicate $)
 
+  $c AntisymRel $. $( Antisymmetric relation predicate $)
+
   $( Extend the definition of a class to include the range Cartesian product
      class. $)
   cxrn $a class ( A |X. B ) $.
@@ -580919,6 +580924,10 @@ A collection of theorems for commuting equalities (or
      elements of ` A ` are disjoint.) $)
   weldisj $a wff ElDisj A $.
 
+  $( Extend the definition of a wff to include the antisymmetry relation
+     predicate.  (Read: ` R ` is an antisymmetric relation.) $)
+  wantisymrel $a wff AntisymRel R $.
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -581024,6 +581033,15 @@ A collection of theorems for commuting equalities (or
       ( wa anbi1i bitri ) ABCGDCGEBDCFHI $.
   $}
 
+  ${
+    bianim.1 $e |- ( ph <-> ( ps /\ ch ) ) $.
+    bianim.2 $e |- ( ch -> ( ps <-> th ) ) $.
+    $( Exchanging conjunction in a biconditional.  (Contributed by Peter Mazsa,
+       31-Jul-2023.) $)
+    bianim $p |- ( ph <-> ( th /\ ch ) ) $=
+      ( wa pm5.32ri bitri ) ABCGDCGECBDFHI $.
+  $}
+
   $( Substitution of equal classes in binary relation.  (Contributed by Peter
      Mazsa, 14-Jun-2024.) $)
   eqbrtr $p |- ( ( A = B /\ B R C ) -> A R C ) $=
@@ -581082,6 +581100,16 @@ A collection of theorems for commuting equalities (or
     ( cv wcel wi cin wa elin imbi1i impexp bitri ralbii2 ) ABEZDFZAGZBCDHZCORFZ
     AGOCFZPIZAGTQGSUAAOCDJKTPALMN $.
 
+  ${
+    $d A y $.  $d x y $.
+    $( Double restricted universal quantification, special case.  (Contributed
+       by Peter Mazsa, 17-Jun-2020.) $)
+    r2alan $p |- ( A. x A. y ( ( ( x e. A /\ y e. B ) /\ ph ) -> ps ) <->
+                   A. x e. A A. y e. B ( ph -> ps ) ) $=
+      ( cv wcel wa wi wal wral impexp 2albii r2al bitr4i ) CGEHDGFHIZAIBJZDKCKQ
+      ABJZJZDKCKSDFLCELRTCDQABMNSCDEFOP $.
+  $}
+
   ${
     3ralbii.1 $e |- ( ph <-> ps ) $.
     $( Inference adding three restricted universal quantifiers to both sides of
@@ -582045,6 +582073,33 @@ relation with an intersection with the same Cartesian product (see also
     ( ccnv crn cres cdm df-rn reseq2i wrel wceq relcnv dfrel5 mpbi eqtri ) ABZA
     CZDNNEZDZNOPNAFGNHQNIAJNKLM $.
 
+  $( Subset of restriction, special case.  (Contributed by Peter Mazsa,
+     10-Apr-2023.) $)
+  relssinxpdmrn $p |- ( Rel R ->
+                        ( R C_ ( S i^i ( dom R X. ran R ) ) <-> R C_ S ) ) $=
+    ( wrel wss cdm crn cxp wa cin relssdmrn biantrud ssin bitr2di ) ACZABDZOAAE
+    AFGZDZHABPIDNQOAJKABPLM $.
+
+  $( Two ways to say that a relation is a subclass.  (Contributed by Peter
+     Mazsa, 11-Apr-2023.) $)
+  cnvref4 $p |- ( Rel R ->
+      ( ( R i^i ( dom R X. ran R ) ) C_ ( S i^i ( dom R X. ran R ) ) <->
+        R C_ S ) ) $=
+    ( wrel cdm crn cxp cin wceq dfrel6 biimpi dmeqd rneqd xpeq12d ineq2d sseq2d
+    wss wb relxp relin2 relssinxpdmrn mp2b sseq1d bitrid bitr3d ) ACZAADZAEZFZG
+    ZBUIDZUIEZFZGZPZUIBUHGZPABPZUEUMUOUIUEULUHBUEUJUFUKUGUEUIAUEUIAHAIJZKUEUIAU
+    QLMNOUNUIBPZUEUPUHCUICUNURQUFUGRAUHSUIBTUAUEUIABUQUBUCUD $.
+
+  ${
+    $d R x y $.
+    $( Two ways to say that a relation is a subclass of the identity relation.
+       (Contributed by Peter Mazsa, 26-Jun-2019.) $)
+    cnvref5 $p |- ( Rel R -> ( R C_ _I <-> A. x A. y ( x R y -> x = y ) ) ) $=
+      ( wrel cid wss cv wbr wi wal ssrel3 wb cvv ideqg elv imbi2i 2albii bitrdi
+      wceq ) CDCEFAGZBGZCHZTUAEHZIZBJAJUBTUASZIZBJAJABCEKUDUFABUCUEUBUCUELBTUAM
+      NOPQR $.
+  $}
+
   ${
     $d A x $.  $d B x $.  $d R x $.  $d V x $.  $d W x $.
     $( Two ways of saying that the coset of ` A ` and the coset of ` B ` have
@@ -582262,6 +582317,12 @@ relation with an intersection with the same Cartesian product (see also
       ZBJDCBDAKPBOCLMN $.
   $}
 
+  $( Intersection with a converse, binary relation.  (Contributed by Peter
+     Mazsa, 24-Mar-2024.) $)
+  brcnvin $p |- ( ( A e. V /\ B e. W ) ->
+                  ( A ( R i^i `' S ) B <-> ( A R B /\ B S A ) ) ) $=
+    ( ccnv cin wbr wa wcel brin brcnvg anbi2d bitrid ) ABCDGZHIABCIZABPIZJAEKBF
+    KJZQBADIZJABCPLSRTQABEFDMNO $.
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -582989,6 +583050,15 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
       ABUSUSCRRUNUOUPUQ $.
   $}
 
+  $( Every class ' R ' restricted to the singleton of the class ' A ' (see
+     ~ ressn2 ) is antisymmetric.  (Contributed by Peter Mazsa,
+     11-Jun-2024.) $)
+  antisymressn $p |-
+      A. x A. y ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) x ) -> x = y ) $=
+    ( cv csn cres wbr wa wceq wi wb cvv brressn el2v simplbi eqtr3 syl2an gen2
+    ) AEZBEZDCFGZHZUATUBHZITUAJZKABUCTCJZUACJZUEUDUCUFTUADHZUCUFUHILABCTUADMMNO
+    PUDUGUATDHZUDUGUIILBACUATDMMNOPTUACQRS $.
+
   $( Any class ' R ' restricted to the singleton of the class ' A ' (see
      ~ ressn2 ) is transitive, see also ~ trrelressn .  (Contributed by Peter
      Mazsa, 16-Jun-2024.) $)
@@ -583954,6 +584024,22 @@ and disjoints ( ~ df-disjs , ~ df-disjALTV ).
       FLCQUEUGUFABUBUCCSTUA $.
   $}
 
+  $( Alternate definition of the converse reflexive relation predicate.
+     (Contributed by Peter Mazsa, 25-May-2024.) $)
+  dfcnvrefrel4 $p |- ( CnvRefRel R <-> ( R C_ _I /\ Rel R ) ) $=
+    ( wcnvrefrel cdm crn cxp cin cid wss wrel df-cnvrefrel cnvref4 bianim ) ABA
+    ACADEZFGMFHAIAGHAJAGKL $.
+
+  ${
+    $d R x y $.
+    $( Alternate definition of the converse reflexive relation predicate.
+       (Contributed by Peter Mazsa, 25-May-2024.) $)
+    dfcnvrefrel5 $p |- ( CnvRefRel R <->
+                         ( A. x A. y ( x R y -> x = y ) /\ Rel R ) ) $=
+      ( wcnvrefrel cid wss wrel cv wbr wceq wi wal dfcnvrefrel4 cnvref5 bianim
+      ) CDCEFCGAHZBHZCIPQJKBLALCMABCNO $.
+  $}
+
   ${
     $d R r $.
     $( Element of the class of converse reflexive relations.  (Contributed by
@@ -586089,6 +586175,58 @@ instead of simply using converse functions (cf. ~ dfdisjALTV ).
   disjALTVxrnidres $p |- Disj ( R |X. ( _I |` A ) ) $=
     ( cid wdisjALTV cres cxrn disjALTVid disjimxrnres ax-mp ) CDBCAEFDGABCHI $.
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Antisymmetry
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  $( Define the antisymmetric relation predicate.  (Read: ` R ` is an
+     antisymmetric relation.)  (Contributed by Peter Mazsa, 24-Jun-2024.) $)
+  df-antisymrel $a |- ( AntisymRel R <->
+                        ( CnvRefRel ( R i^i `' R ) /\ Rel R ) ) $.
+
+  $( Alternate definition of the antisymmetric relation predicate.
+     (Contributed by Peter Mazsa, 24-Jun-2024.) $)
+  dfantisymrel4 $p |- ( AntisymRel R <->
+                        ( ( R i^i `' R ) C_ _I /\ Rel R ) ) $=
+    ( wantisymrel ccnv cin wcnvrefrel cid wss df-antisymrel relcnv relin2 ax-mp
+    wrel dfcnvrefrel4 mpbiran2 bianbi ) ABAACZDZEZALQFGZAHRSQLZPLTAIAPJKQMNO $.
+
+  ${
+    $d R x y $.
+    $( Alternate definition of the antisymmetric relation predicate.
+       (Contributed by Peter Mazsa, 24-Jun-2024.) $)
+    dfantisymrel5 $p |- ( AntisymRel R <->
+        ( A. x A. y ( ( x R y /\ y R x ) -> x = y ) /\ Rel R ) ) $=
+      ( wantisymrel ccnv cin wcnvrefrel wrel cv wa wceq wi df-antisymrel relcnv
+      wbr wal relin2 ax-mp dfcnvrefrel5 cvv mpbiran2 brcnvin el2v imbi1i 2albii
+      wb bitri bianbi ) CDCCEZFZGZCHAIZBIZCOUMULCOJZULUMKZLZBPAPZCMUKULUMUJOZUO
+      LZBPAPZUQUKUTUJHZUIHVACNCUIQRABUJSUAUSUPABURUNUOURUNUFABULUMCCTTUBUCUDUEU
+      GUH $.
+  $}
+
+  ${
+    $d A x y $.  $d R x y $.
+    $( (Contributed by Peter Mazsa, 25-Jun-2024.) $)
+    antisymrelres $p |- ( AntisymRel ( R |` A ) <->
+        A. x e. A A. y e. A ( ( x R y /\ y R x ) -> x = y ) ) $=
+      ( cres wantisymrel cv wbr wa wceq wi wal wcel wral wrel relres wb cvv elv
+      brres dfantisymrel5 mpbiran2 anbi12i bitri imbi1i 2albii r2alan 3bitri
+      an4 ) DCEZFZAGZBGZUJHZUMULUJHZIZULUMJZKZBLALZULCMZUMCMZIULUMDHZUMULDHZIZI
+      ZUQKZBLALVDUQKBCNACNUKUSUJODCPABUJUAUBURVFABUPVEUQUPUTVBIZVAVCIZIVEUNVGUO
+      VHUNVGQBCULUMDRTSUOVHQACUMULDRTSUCUTVBVAVCUIUDUEUFVDUQABCCUGUH $.
+  $}
+
+  ${
+    $d A x y $.  $d R x y $.
+    $( (Contributed by Peter Mazsa, 29-Jun-2024.) $)
+    antisymrelressn $p |- AntisymRel ( R |` { A } ) $=
+      ( vx vy csn cres wantisymrel cv wbr wa wceq wi antisymressn dfantisymrel5
+      wal wrel relres mpbir2an ) BAEZFZGCHZDHZTIUBUATIJUAUBKLDOCOTPCDABMBSQCDTN
+      R $.
+  $}
+
 $( (End of Peter Mazsa's mathbox.) $)
 $( End $[ set-mbox-pm.mm $] $)