dfcnvrefrel4 eqvrel1cossressn

set.mm

@@ -551602,6 +551602,40 @@ equivalence of domain elementhood (equivalence is not necessary as
     DIZPCJDABGZKEQLCHDABCMDQCNO $.
   $}
 
+  $( Two ways to say that a relation is a subclass.  (Contributed by Peter
+     Mazsa, 25-May-2024.) $)
+  cnvref4 $p |- ( Rel R ->
+                  ( R C_ S <-> R C_ ( S i^i ( dom R X. ran R ) ) ) ) $=
+    ( wrel wss cdm crn cxp wa cin relssdmrn biantrud ssin syl6bb ) AC
+    ZABDZOAAEAFGZDZHABPIDNQOAJKABPLM $.
+
+  ${
+    $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 wceq ssrel3 wb cvv ideqg elv imbi2i
+    2albii syl6bb ) CDCEFAGZBGZCHZTUAEHZIZBJAJUBTUAKZIZBJAJABCELUDUFA
+    BUCUEUBUCUEMBTUANOPQRS $.
+  $}
+
+  ${
+    $d R x $.
+    $( The domain of the intersection of a reflexive class with its converse
+       is the intersection of the domain and range of the class.  Compare with
+       ~ dmin and ~ dfrefrel5 .   (Contributed by Peter Mazsa,
+       25-May-2024.) $)
+    refdmincnv $p |- ( A. x e. ( dom R i^i ran R ) x R x ->
+                       dom ( R i^i `' R ) = ( dom R i^i ran R ) ) $=
+      ( cv wbr cdm crn cin wral ccnv wss wa wceq cvv brcnvg el2v anbi2i
+    wb anidm sylbir sylibr bitri ralbii df-rn ineq2i raleqi wcel brin
+    bitr4i vex breldm ralimi dfss3 dmin jctil eqss syl6eqr ) ACZUQBDZ
+    ABEZBFZGZHZBBIZGZEZUSVCEZGZVAVBVEVGJZVGVEJZKVEVGLVBVIVHVBURUQUQVC
+    DZKZAVGHZVIVLURAVGHVBVKURAVGVKURURKURVJURURVJURQAAUQUQMMBNOPURRUA
+    UBURAVAVGUTVFUSBUCUDZUEUHVLUQVEUFZAVGHVIVKVNAVGVKUQUQVDDVNUQUQBVC
+    UGUQUQVDAUIZVOUJSUKAVGVEULTSBVCUMUNVEVGUOTVMUP $.
+  $}
+
   $( Absorption law for intersection.  This is ~ inabs3 in Glauco Siliprandi's
      Mathbox: when we cut and paste that into main, delete this.  (Contributed
      by Glauco Siliprandi, 17-Aug-2020.) $)
@@ -555354,6 +555388,22 @@ and disjoints ( ~ df-disjs , ~ df-disjALTV ).
       UBPZUFLCQUEUIUFABUBUCCSTUA $.
   $}
 
+  $( 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 cid cdm crn cxp cin wss wrel wa dfcnvrefrel2 cnvref4
+    pm5.32ri bitr4i ) ABACADAEFGHZAIZJACHZPJAKPQOACLMN $.
+
+  ${
+    $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
@@ -556925,6 +556975,22 @@ of negatively transitive relations ( ~ df-negtrrels ) is equivalent to
       ADBCQADBCSR $.
   $}
 
+  ${
+    $d A a u v w $.  $d R a u v w $. $d V u v w $.
+    $( Cosets restricted to singleton is an equivalence relation.
+       (Contributed by Peter Mazsa, 27-May-2024.)  $)
+    eqvrel1cossressn $p |- ( A e. V -> EqvRel ,~ ( R |` { A } ) ) $=
+      ( vu vv vw va cv wbr wa wal wrex wb br1cossres el2v breq1 anbi12d
+    cvv rexsng syl5bb wcel csn cres ccoss wi weqvrel wceq an3 sylibrd
+    syl6bi alrimivv alrimiv eqvrelcoss3 sylibr ) ACUAZDHZEHZBAUBZUCZU
+    DZIZUQFHZUTIZJZUPVBUTIZUEZFKEKZDKUTUFUOVGDUOVFEFUOVDAUPBIZAVBBIZJ
+    ZVEUOVDVHAUQBIZJZVKVIJZJVJUOVAVLVCVMVAGHZUPBIZVNUQBIZJZGURLZUOVLV
+    AVRMDEGURUPUQBRRNOVQVLGACVNAUGZVOVHVPVKVNAUPBPZVNAUQBPZQSTVCVPVNV
+    BBIZJZGURLZUOVMVCWDMEFGURUQVBBRRNOWCVMGACVSVPVKWBVIWAVNAVBBPZQSTQ
+    VHVKVKVIUHUJVEVOWBJZGURLZUOVJVEWGMDFGURUPVBBRRNOWFVJGACVSVOVHWBVI
+    VTWEQSTUIUKULDEFUSUMUN $.
+  $}
+
   $( Alternate definition of the coelement equivalence relations class.  Other
      alternate definitions should be based on ~ eqvrelcoss2 , ~ eqvrelcoss3 and
      ~ eqvrelcoss4 when needed.  (Contributed by Peter Mazsa, 22-Nov-2023.) $)