misc order

mazsa · Jul 20, 2024 · 3acb85c · 3acb85c
1 parent 5a78c5e
commit 3acb85c
Showing 1 changed file with 229 additions and 24 deletions.
diff --git a/set.mm b/set.mm
@@ -550629,6 +550629,11 @@ A collection of theorems for commuting equalities (or
       ( wceq sseq bicomd ) CDGABABCDEFHI $.
   $}
 
+  $( (Contributed by Peter Mazsa, 18-Jul-2024.) $)
+  2eq0or $p |- ( ( A = (/) \/ B = (/) ) -> ( A i^i B ) = (/) ) $=
+    ( c0 wceq cin ineq1 0in syl6eq ineq2 in0 jaoi ) ACDZABEZCDBCDZLMC
+    BECACBFBGHNMACECBCAIAJHK $.
+
  $( Two ways of expressing the restriction of an intersection.  (Contributed
      by Peter Mazsa, 5-Jun-2021.) $)
   inres2 $p |- ( ( R |` A ) i^i S ) = ( ( R i^i S ) |` A ) $=
@@ -550905,6 +550910,21 @@ A collection of theorems for commuting equalities (or
     ZDLUGUEJZDLUDUFUBUKULDUJULEACUHAJUIUEUGUHABMNOPEDUCBRDUESTUA $.
   $}
 
+  ${
+    $d A x $.
+    $( (Contributed by Peter Mazsa, 18-Jul-2024.) $)
+    eq02 $p |- ( A = (/) <-> ( A. x e. A ph /\ -. E. x e. A ph ) ) $=
+      ( c0 wne wn wral wrex wi wceq r19.2zb notbii nne pm4.61 3bitr3i
+    wa ) CDEZFABCGZABCHZIZFCDJRSFPQTABCKLCDMRSNO $.
+  $}
+
+  ${
+    $d A x $.
+    $( (Contributed by Peter Mazsa, 18-Jul-2024.) $)
+    eq02im $p |- ( A = (/) -> -. E. x e. A ph ) $=
+      ( c0 wceq wral wrex wn eq02 simprbi ) CDEABCFABCGHABCIJ $.
+  $}
+
   $( Negated elementhood of ordered pair.  (Contributed by Peter Mazsa,
      14-Jan-2019.) $)
   opelvvdif $p |- ( ( A e. V /\ B e. W ) ->
@@ -551100,6 +551120,50 @@ A collection of theorems for commuting equalities (or
       $.
   $}
 
+  ${
+    $d A x y $.
+    $( (Contributed by Peter Mazsa, 16-Jul-2024.) $)
+    reldm2 $p |- ( Rel A -> dom A = { y | E. x e. A y = ( 1st ` x ) } ) $=
+      ( wrel c1st cfv wceq wrex cdm wcel releldm2 rexbii syl6bb abbi2dv
+    cv eqcom ) CDZBOZAOEFZGZACHZBCIZQRUBJSRGZACHUAACRKUCTACSRPLMN $.
+  $}
+
+  ${
+    $d A x $.  $d B x $.
+    $( (Contributed by Peter Mazsa, 16-Jul-2024.) $)
+    op2ndeq $p |- ( A e. ( V X. W ) ->
+                    ( ( 2nd ` A ) = B <-> E. x A = <. x , B >. ) ) $=
+      ( cxp wcel cvv c2nd cfv wceq cv cop wex wb xpss sseli wa c1st syl
+    eqid eqopi mpanr1 fvex opeq1 eqeq2d spcev ex simpr syl6bi exlimdv
+    eqop impbid ) BDEFZGBHHFZGZBIJCKZBALZCMZKZANZOUNUOBDEPQUPUQVAUPUQ
+    VAUPUQRBBSJZCMZKZVAUPVBVBKUQVDVBUABVBCHHUBUCUTVDAVBBSUDURVBKUSVCB
+    URVBCUEUFUGTUHUPUTUQAUPUTVBURKZUQRUQBURCHHULVEUQUIUJUKUMT $.
+  $}
+
+  ${
+    $d A x y $.  $d B x y $.
+    $( (Contributed by Peter Mazsa, 16-Jul-2024.) $)
+    relelrn2 $p |- ( Rel A ->
+                     ( B e. ran A <-> E. x e. A ( 2nd ` x ) = B ) ) $=
+      ( vy wrel crn wcel cv c2nd cfv wceq wrex cvv elex anim2i fvex wex
+    wa id wb syl6eqelr rexlimivw cop elrn2g adantl cxp wi df-rel ssel
+    wss sylbi imp op2ndeq rexbidva adantr rexcom4 risset exbii bitr4i
+    syl syl6bb bitr4d pm5.21nd ) BEZCBFZGZAHZIJZCKZABLZVDCMGZRZVFVKVD
+    CVENOVJVKVDVIVKABVICVHMVISVGIPUAUBOVLVFDHCUCZBGZDQZVJVKVFVOTVDDCB
+    MUDUEVLVJVGVMKZDQZABLZVOVDVJVRTVKVDVIVQABVDVGBGZRVGMMUFZGZVIVQTVD
+    VSWAVDBVTUJVSWAUGBUHBVTVGUIUKULDVGCMMUMUTUNUOVRVPABLZDQVOVPADBUPV
+    NWBDAVMBUQURUSVAVBVC $.
+  $}
+
+  ${
+    $d A x y $.
+    $( (Contributed by Peter Mazsa, 16-Jul-2024.) $)
+    relrn2 $p |- ( Rel A -> ran A = { y | E. x e. A y = ( 2nd ` x ) } ) $=
+      ( wrel c2nd cfv wceq wrex crn wcel relelrn2 eqcom rexbii syl6bb
+      cv abbi2dv ) CDZBOZAOEFZGZACHZBCIZQRUBJSRGZACHUAACRKUCTACSRLMNP
+      $.
+  $}
+
   ${
     eceq1i.1 $e |- A = B $.
     $( Equality theorem for ` C ` -coset of ` A ` and ` C ` -coset of ` B ` ,
@@ -552201,6 +552265,15 @@ relation with an intersection with the same Cartesian product (see also
       HZBHZCIQPCIJBKAKCLABCMN $.
   $}
 
+  ${
+    $d R x y $.
+    $( (Contributed by Peter Mazsa, 15-Jul-2024.) $)
+    relcnveq5 $p |- ( Rel R ->
+        ( A. x A. y ( x R y -> y R x ) <-> A. x A. y ( x R y <-> y R x ) ) ) $=
+      ( cv wbr wi wal ccnv wss wrel wb cnvsym relcnveq4 syl5bbr ) ADZBD
+    ZCEZPOCEZFBGAGCHCICJQRKBGAGABCLABCMN $.
+  $}
+
   ${
     $d A u v $.  $d R u v $.
     $( Simplification of a special quotient set.  (Contributed by Peter Mazsa,
@@ -552655,15 +552728,22 @@ relation with an intersection with the same Cartesian product (see also
     DEABCQT $.
   $}
 
-  $( Implication of two reflexive relations (when T = _I ). (Contributed by
-     Peter Mazsa, 7-May-2024.) $)
+  $( (Contributed by Peter Mazsa, 7-May-2024.) $)
   asymcnvepres $p |- A. x A. y ( x ( `' _E |` A ) y ->
                                  -. y ( `' _E |` A ) x ) $=
     ( cv cep ccnv cres wbr wn wi wa wb cvv brcnvepres elnotel intnand
     wcel el2v adantl sylnibr sylbi gen2 ) ADZBDZEFCGZHZUDUCUEHZIZJABU
     FUCCQZUDUCQZKZUHUFUKLABCUCUDMMNRUKUDCQZUCUDQZKZUGUJUNIUIUJUMULUDU
     COPSUGUNLBACUDUCMMNRTUAUB $.
 
+  $( (Contributed by Peter Mazsa, 14-Jul-2024.) $)
+  asymALTcnvepres $p |- 
+      A. x e. B A. y e. C ( x ( `' _E |` A ) y -> -. y ( `' _E |` A ) x ) $=
+    ( cv cep ccnv cres wbr wn wi wa wb cvv brcnvepres elnotel intnand
+    wcel el2v adantl sylnibr sylbi rgen2w ) AFZBFZGHCIZJZUFUEUGJZKZLA
+    BDEUHUECSZUFUESZMZUJUHUMNABCUEUFOOPTUMUFCSZUEUFSZMZUIULUPKUKULUOU
+    NUFUEQRUAUIUPNBACUFUEOOPTUBUCUD $.
+
   $( Implication of two reflexive relations (when T = _I ). (Contributed by
      Peter Mazsa, 7-May-2024.) $)
   indmrnin $p |- ( ( ( T i^i ( dom R X. ran R ) ) C_ R /\
@@ -554957,6 +555037,60 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
     ) BEGBCAHZIJGFKZBCLZFRMADGABCLZFRBCENTUAFADSABCOPQ $.
   $}
 
+  ${
+    $d A y $.  $d R y $.  $d V y $.
+    $( (Contributed by Peter Mazsa, 17-Jul-2024.) $)
+    rnressn $p |- ( ( A e. V \/ Rel R ) ->
+                    ran ( R |` { A } ) = { y | A R y } ) $=
+      ( wcel csn cres crn cv wbr cab wceq wrel wb cvv elrnressn abbi2dv
+    elvd cima df-ima relimasn syl5eqr jaoi ) BDEZCBFZGHZBAIZCJZAKZLCM
+    ZUDUHAUFUDUGUFEUHNABUGCDOPRQUJUFCUESUICUETABCUAUBUC $.
+  $}
+
+  ${
+    $d A x y $.  $d R x y $.
+    $( (Contributed by NM, 8-May-2005.)  (Revised by Peter Mazsa,
+       17-Jul-2024.) $)
+    imasn $p |- ( ( A e. V \/ Rel R ) -> ( R " { A } ) = { y | A R y } ) $=
+      ( vx wcel csn cima cv wbr cab wceq wrel elex wrex dfima2 breq1 wn
+    cvv c0 rexsng abbidv syl5eq syl wa snprc imaeq2 sylbi ima0 syl6eq
+    adantl wex brrelex1 stoic1a nexdv abn0 necon1bbii sylib eqtr4d ex
+    pm2.61d2 jaoi ) BDFZCBGZHZBAIZCJZAKZLZCMZVCBSFZVIBDNVKVEEIZVFCJZE
+    VDOZAKVHEACVDPVKVNVGAVMVGEBSVLBVFCQUAUBUCZUDVJVKVIVJVKRZVIVJVPUEZ
+    VETVHVPVETLVJVPVECTHZTVPVDTLVEVRLBUFVDTCUGUHCUIUJUKVQVGAULZRVHTLV
+    QVGAVJVGVKBVFCUMUNUOVSVHTVGAUPUQURUSUTVOVAVB $.
+  $}
+
+  ${
+    $d A y $.  $d R y $.  $d V y $.
+    $( (Contributed by Peter Mazsa, 17-Jul-2024.) $)
+    imasn2 $p |- ( ( A e. V \/ Rel R ) ->
+                   ( R " { A } ) = ran ( R |` { A } ) ) $=
+      ( vy wcel wrel wo csn cima wbr cab cres crn imasn rnressn eqtr4d
+    cv ) ACEBFGBAHZIADQBJDKBRLMDABCNDABCOP $.
+  $}
+
+  ${
+    $d A y $.  $d R y $.
+    $( Alternate definition of ` R ` -coset of ` A ` .  Definition 34 of
+       [Suppes] p. 81.  (Contributed by NM, 3-Jan-1997.)  (Proof shortened by
+       Mario Carneiro, 9-Jul-2014.)  (Revised by Peter Mazsa, 5-Sep-2023.) $)
+    dfec2ALTV $p |- (  ( A e. V \/ Rel R ) -> [ A ] R = { y | A R y } ) $=
+      ( wcel wrel wo cec csn cima cv wbr cab df-ec imasn syl5eq ) BDECF
+    GBCHCBIJBAKCLAMBCNABCDOP $.
+  $}
+
+  ${
+    $d A x $. $d B x $. $d R x $.
+    $( (Contributed by Peter Mazsa, 11-Apr-2019.)  (Revised by Peter Mazsa,
+       17-Jul-2024.) $)
+    eqec $p |- ( ( B e. V \/ Rel R ) ->
+                 ( A = [ B ] R <-> A. x ( x e. A <-> B R x ) ) ) $=
+      ( wcel wrel wo cec wceq cv wbr wb dfec2ALTV eqeq2d abeq2 syl6bb
+      cab wal ) CEFDGHZBCDIZJBCAKZDLZARZJUBBFUCMASTUAUDBACDENOUCABPQ
+      $.
+  $}
+
   $( (Contributed by Peter Mazsa, 12-Jun-2024.) $)
   elrnressn2 $p |- ( ( A e. V /\ B e. W ) ->
       ( B e. ran ( R |` { A } ) <-> B e. [ A ] R ) ) $=
@@ -554965,10 +555099,10 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
 
   ${
     $d A x $.  $d R x $.  $d V x $.
-    $( (Contributed by Peter Mazsa, 12-Jun-2024.) $)
-    dfec3 $p |- ( A e. V -> [ A ] R = ran ( R |` { A } ) ) $=
-      ( vx wcel csn cres crn cec cv wb cvv elrnressn2 elvd eqrdv eqcomd
-    ) ACEZBAFGHZABIZQDRSQDJZRETSEKDATBCLMNOP $.
+    $( (Contributed by Peter Mazsa, 17-Jul-2024.) $)
+    dfec3 $p |- ( ( A e. V \/ Rel R ) -> [ A ] R = ran ( R |` { A } ) ) $=
+      ( wcel wrel wo cec csn cima cres crn df-ec imasn2 syl5eq ) ACDB
+      EFABGBAHZIBOJKABLABCMN $.
   $}
 
   ${
@@ -555023,6 +555157,17 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
     JZDAKDAUCCMUHUJDAUHUIUGJUJUEUIUGUEUINDUDBROSPUDBUFCQTUAUB $.
   $}
 
+  ${
+    $d A x y $.  $d B x y $.  $d R x y $.
+    $( (Contributed by Peter Mazsa, 17-Jul-2024.) $)
+    elressn $p |- ( A e. V ->
+        ( B e. ( R |` { A } ) <-> E. y ( B = <. A , y >. /\ A R y ) ) ) $=
+      ( vx csn cres wcel cv cop wceq wa wex wrex wbr elres opeq1 eqeq2d
+    eleq1d df-br syl6bbr anbi12d exbidv rexsng syl5bb ) CDBGZHICFJZAJ
+    ZKZLZUJDIZMZANZFUGOBEICBUIKZLZBUIDPZMZANZFACDUGQUNUSFBEUHBLZUMURA
+    UTUKUPULUQUTUJUOCUHBUIRZSUTULUODIUQUTUJUODVATBUIDUAUBUCUDUEUF $.
+  $}
+
   ${
     $d A x $.  $d V x $.
     $( Any class ' R ' restricted to the singleton of the set ' A ' (see
@@ -555130,19 +555275,20 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
 
   ${
     $d A y $. $d B y $. $d R y $. $d W y $.
-    $( (Contributed by Peter Mazsa, 14-Jun-2024.) $)
-    ecressn $p |- ( ( A e. V /\ B e. W ) ->
+    $( cf dmressnqs (Contributed by Peter Mazsa, 14-Jun-2024.) $)
+    ecressn $p |- ( ( ( A e. V \/ Rel R ) /\ B e. W ) ->
                     ( [ B ] ( R |` { A } ) = [ A ] R \/
                       [ B ] ( R |` { A } ) = (/) ) ) $=
-      ( vy wcel wa wceq cv wbr csn cres cec nfvd cab wb cvv elecressn
-      elvd eqbrb syl6bb abbi2dv adantl dfec2 adantr a0orb ) ADGZBEGZH
-      ZBAIZAFJZCKZFBCALMNZACNZUJUKFOUIUNUKUMHZFPIUHUIUPFUNUIULUNGZUKB
-      ULCKHZUPUIUQURQFABULCERSTBAULCUAUBUCUDUHUOUMFPIUIFACDUEUFUG $.
+      ( vy wcel wrel wo wa wceq cv wbr csn cres cec nfvd cab wb cvv
+    elecressn elvd eqbrb syl6bb abbi2dv adantl dfec2ALTV adantr a0orb
+    ) ADGCHIZBEGZJZBAKZAFLZCMZFBCANOPZACPZULUMFQUKUPUMUOJZFRKUJUKURFU
+    PUKUNUPGZUMBUNCMJZURUKUSUTSFABUNCETUAUBBAUNCUCUDUEUFUJUQUOFRKUKFA
+    CDUGUHUI $.
   $}
 
   ${
     $d A x y $. $d B x y $. $d R x y $. $d V y $. $d W x y $.
-    $( (Contributed by Peter Mazsa, 1-Jun-2024.) $)
+    $( cf dmressnqs (Contributed by Peter Mazsa, 1-Jun-2024.) $)
     ec1cossressn $p |- ( ( A e. V /\ B e. W ) ->
                          ( [ B ] ,~ ( R |` { A } ) = [ A ] R \/
                            [ B ] ,~ ( R |` { A } ) = (/) ) ) $=
@@ -555153,22 +555299,55 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
       CSURAUMCSUBUCUDUEUIUQUNFQRUJFACDUFUGUH $.
   $}
 
-  $( (Contributed by Peter Mazsa, 14-Jun-2024.) $)
-  ecressn2 $p |- ( A e. V ->
+  $( cf dmressnqs (Contributed by Peter Mazsa, 14-Jun-2024.) $)
+  ecressn2 $p |- ( ( A e. V \/ Rel R ) ->
       ( B e. dom ( R |` { A } ) -> [ B ] ( R |` { A } ) = [ A ] R ) ) $=
-    ( wcel csn cres cdm cec wceq wa c0 wo ecressn wn wi ecdmn0 biimpi
-    wne adantl df-ne sylib orel2 syl mpd ex ) ADEZBCAFGZHZEZBUHIZACIJ
-    ZUGUJKZULUKLJZMZULABCDUINUMUNOZUOULPUMUKLSZUPUJUQUGUJUQBUHQRTUKLU
-    AUBUNULUCUDUEUF $.
+    ( wcel wrel wo csn cres cdm cec wa c0 ecressn wn wi ecdmn0 biimpi
+    wceq wne adantl df-ne sylib orel2 syl mpd ex ) ADECFGZBCAHIZJZEZB
+    UIKZACKSZUHUKLZUMULMSZGZUMABCDUJNUNUOOZUPUMPUNULMTZUQUKURUHUKURBU
+    IQRUAULMUBUCUOUMUDUEUFUG $.
 
-  $( (Contributed by Peter Mazsa, 9-Jun-2024.) $)
+  $( cf dmressnqs (Contributed by Peter Mazsa, 9-Jun-2024.) $)
   ec1cossressn2 $p |- ( A e. V ->
       ( B e. dom ,~ ( R |` { A } ) -> [ B ] ,~ ( R |` { A } ) = [ A ] R ) ) $=
     ( wcel csn cres ccoss cdm wceq wa c0 wo ec1cossressn wn wi ecdmn0
     cec wne biimpi adantl df-ne sylib orel2 syl mpd ex ) ADEZBCAFGHZI
     ZEZBUIRZACRJZUHUKKZUMULLJZMZUMABCDUJNUNUOOZUPUMPUNULLSZUQUKURUHUK
     URBUIQTUAULLUBUCUOUMUDUEUFUG $.
 
+  ${
+    $d A x y $. $d B x y $. $d R x y $. $d V y $.
+    $( (Contributed by Peter Mazsa, 18-Jul-2024.) $)
+    dmressnqs $p |- ( dom ( R |` { A } ) /. ( R |` { A } ) ) =
+                    if ( A e. dom R , { [ A ] R } , (/) ) $=
+      ( vy vx csn cdm wcel cec c0 wceq wi wn cab cin cv wa wrex wb wo
+      cvv cres cqs cif df-qs wrel ecressn2 imp eqeq2d rexbidva df-rex
+      orcs wex eldmressnALTV anbi1i anass bitri exbii bitr2i ceqsexgv
+      elv biidd syl5bbr bitrd abbidv syl5eq ineq2i inab eqtr2i syl6eq
+      df-sn wal ax-5 bj-abv ineq1 incom inv1 eqtri 3syl eqtrd biimpri
+      ianor olcs sylnibr eq0rdv eq02im syl bj-ab0 eqeq1i sylibr ifval
+      alrimiv mpbir2an ) BAEUAZFZWMUBZABFZGZABHZEZIUCJWQWOWSJKWQLZWOI
+      JZKWQWOWQCMZWSNZWSWQWOWQCOZWRJZPZCMZXCWQWOXDDOZWMHZJZDWNQZCMZXG
+      DCWNWMUDZWQXKXFCWQXKXEDWNQZXFWQBUEZXKXNRWQXOSZXJXEDWNXPXHWNGZPX
+      IWRXDXPXQXIWRJAXHBWPUFUGUHUIUKXNXHAJZXFPZDULZWQXFXNXQXEPZDULXTX
+      EDWNUJYAXSDYAXRWQPZXEPXSXQYBXEXQYBRDAXHBTUMUTZUNXRWQXEUOUPUQURX
+      FXFDAWPXRXFVAUSVBVCVDVEXCXBXECMZNXGWSYDXBCWRVJVFWQXECVGVHVIWQWQ
+      CVKXBTJZXCWSJWQCVLWQCVMYEXCTWSNZWSXBTWSVNYFWSTNWSTWSVOWSVPVQVIV
+      RVSWTXLIJZXAWTXKLZCVKYGWTYHCWTWNIJYHWTDWNWTYBXQXRLZWTYBLZYJYIWT
+      SXRWQWAVTWBYCWCWDXJDWNWEWFWKXKCWGWFWOXLIXMWHWIWQWOWSIWJWL $.
+  $}
+
+  $( (Contributed by Peter Mazsa, 19-Jul-2024.) $)
+  dmressnqseq $p |- if- ( A e. dom R ,
+      ( ( dom ( R |` { A } ) /. ( R |` { A } ) ) = { A } <-> [ A ] R = A ) ,
+      ( ( dom ( R |` { A } ) /. ( R |` { A } ) ) = { A } <-> -. A e. _V ) ) $=
+    ( cdm wcel csn cres cqs wceq cec wb cvv wn wi wa c0 syl5eq eqeq1d
+    wif cif eqcom dmressnqs iftrue sneqbg 3bitr3g bitrd iffalse snprc
+    bitri syl6bbr pm3.2i dfifp2 mpbir ) ABCZDZBAEZFZCUPGZUOHZABIZAHZJ
+    ZURAKDLZJZRUNVAMZUNLZVCMZNVDVFUNURUSEZUOHZUTUNUQVGUOUNUQUNVGOSZVG
+    ABUAZUNVGOUBPQUNUOVGHAUSHVHUTAUSUMUCUOVGTAUSTUDUEVEUROUOHZVBVEUQO
+    UOVEUQVIOVJUNVGOUFPQVBUOOHVKAUGUOOTUHUIUJUNVAVCUKUL $.
+
   ${
     $d A u x $.
     $( erimsn cf. ~ 0nep0 . (Contributed by Peter Mazsa, 15-Jun-2024.) $)
@@ -555336,10 +555515,11 @@ range of a range Cartesian product ( ~ dfcoss4 ), but neither of these
 
   $( The domain of cosets of a restriction to a singleton is the ` R ` -coset
      of the element of the singleton.  (Contributed by Peter Mazsa,
-     13-Jun-2024.) $)
-  dm1cossressn $p |- ( A e. V -> dom ,~ ( R |` { A } ) = [ A ] R ) $=
-    ( wcel cec csn cres crn ccoss cdm dfec3 dmcoss2 syl6reqr ) ACDABE
-    BAFGZHNIJABCKNLM $.
+     17-Jul-2024.) $)
+  dm1cossressn $p |- ( ( A e. V \/ Rel R ) ->
+                       dom ,~ ( R |` { A } ) = [ A ] R ) $=
+    ( wcel wrel wo cec csn cres crn ccoss cdm dfec3 dmcoss2 syl6reqr
+    ) ACDBEFABGBAHIZJPKLABCMPNO $.
 
   $( The domain of cosets of the restricted converse epsilon relation is the
      union of the restriction.  (Contributed by Peter Mazsa, 18-May-2019.)
@@ -556070,6 +556250,14 @@ definitions of epsilon relation ( ~ df-eprel ) and identity relation
     ( cincomparelALTto cdm cdif dfincomparelALTto dmrnxpdifincnvdif
     crn cxp ccnv cin cun eqtri ) ABACZAGZHADZOIJMNJZPHAAIKDAEAFL $.
 
+  $( (Contributed by Peter Mazsa, 20-Jul-2024.) $)
+  incompareltovvdif $p |- ( Rel R ->
+      InCompaRelTo ( ( _V X. _V ) \ R ) = ( R i^i `' R ) ) $=
+    ( wrel cvv cxp cdif cincomparelto ccnv cin dfincomparelto relddif
+    wceq cnvxpdif difeq2i eqtri relcnv ax-mp a1i ineq12d syl5eq ) ABZ
+    CCDZAEZFUAUBEZUCGZHAAGZHUBITUCAUDUEAJUDUEKTUDUAUAUEEZEZUEUDUAUBGZ
+    EUGCCUBLUHUFUACCALMNUEBUGUEKAOUEJPNQRS $.
+
   $( (Contributed by Peter Mazsa, 13-Jul-2024.) $)
   incomparelALTtovvdif $p |- ( R e. V -> ( Rel R ->
       InCompaRelALTTo ( ( _V X. _V ) \ R ) = ( R i^i `' R ) ) ) $=
@@ -557536,6 +557724,23 @@ class of symmetric relations as well (like the elements of the class of
     ( cep ccnv cres cin wasymrel c0 wceq wrel asymincnvepres relinres
     dfasymrel4 mpbir2an ) BCDZAEFZGPPDFHIPJABKABOLPMN $.
 
+  $( (Contributed by Peter Mazsa, 20-Jul-2024.) $)
+  incompareltovvdifcnvepres $p |-
+      InCompaRelTo ( ( _V X. _V ) \ ( `' _E |` A ) ) = (/) $=
+    ( cvv cxp cep ccnv cres cdif cincomparelto c0 cin asymrelcnvepres
+    wceq wasymrel wrel relres dfasymrel4 mpbi incompareltovvdif ax-mp
+    mpbiran2 eqeq1i mpbir ) BBCDEZAFZGHZILUDUDEJZILZUDMZUGAKUHUGUDNZU
+    CAOZUDPTQUEUFIUIUEUFLUJUDRSUAUB $.
+
+  $( (Contributed by Peter Mazsa, 20-Jul-2024.) $)
+  incomparelALTtovvdifcnvepres $p |- ( A e. V ->
+      InCompaRelALTTo ( ( _V X. _V ) \ ( `' _E |` A ) ) = (/) ) $=
+    ( wcel cvv cxp cep ccnv cres cdif cincomparelALTto cin cnvepresex
+    c0 wceq wrel relres incomparelALTtovvdif mpi syl wasymrel syl6eq
+    asymrelcnvepres dfasymrel4 mpbiran2 mpbi ) ABCZDDEFGZAHZIJZUHUHGK
+    ZMUFUHDCZUIUJNZABLUKUHOZULUGAPZUHDQRSUHTZUJMNZAUBUOUPUMUNUHUCUDUE
+    UA $.
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Strict completeness (converse asymmetry)