got rid of releqopab in favor of opabbi2i

ZhihanLiphys · Apr 19, 2021 · 7456ab4 · 7456ab4
1 parent 300b604
commit 7456ab4
Showing 1 changed file with 61 additions and 84 deletions.
diff --git a/nf.mm b/nf.mm
@@ -54947,19 +54947,6 @@ result of an operator (deduction version).  (Contributed by Paul
       UITVSVNEIDOVKVNVBEDVTUJGTUKULUNVLBUOUPUQVCVGVBEVTFURUSBVBCUTVA $.
   $}
 
-  ${
-    $d A x y z $.  $d ph z $.
-    releqopab.1 $e |- ( <. x , y >. e. A <-> ph ) $.
-    $( Equality condition for an ordered pair abstraction.  (Contributed by SF,
-       18-Feb-2015.) $)
-    releqopab $p |- ( ( _V X. _V ) i^i A ) = { <. x , y >. | ph } $=
-      ( vz cvv cxp cin cv cop wceq wa wex cab copab wcel elvv anbi1i elin eleq1
-      19.41vv 3bitr4i syl6bb pm5.32i 2exbii bitri abbi2i df-opab eqtr4i ) GGHZD
-      IZFJZBJCJKZLZAMZCNBNZFOABCPUQFULUMULQZUOUMDQZMZCNBNZUQUMUKQZUSMUOCNBNZUSM
-      URVAVBVCUSBCUMRSUMUKDTUOUSBCUBUCUTUPBCUOUSAUOUSUNDQAUMUNDUAEUDUEUFUGUHABC
-      FUIUJ $.
-  $}
-
   ${
     $d A x $.  $d A z $.  $d R x $.  $d R y $.  $d R z $.  $d V y $.  $d V z $.
     $d x y $.  $d x z $.  $d y z $.
@@ -56382,39 +56369,29 @@ result of an operator (deduction version).  (Contributed by Paul
     $( The class of all symmetric relationships is a set.  (Contributed by SF,
        20-Feb-2015.) $)
     symex $p |- Sym e. _V $=
-      ( vx vy vr va vp cvv csset ccnv c1c cv wbr wral wcel cop brcnv wa 3bitr4i
-      wex anbi12i 3bitri csym cxp cswap cimage ctxp crn cdif c1st c2nd cin csi3
-      cins2 cins4 cima ccompl copab df-sym wel wceq eleq1 df-br syl6bbr imbi12d
-      wi bitr3i ralxp wn wrex csn oteltxp eldif trtxp vex brssetsn bitri dfcnv2
-      eqeq2i ancom exbii elrn cnvex clel3 opelssetsn notbii annim elin otelins2
-      brimage oqelins4 otsnelsi3 opelxp mpbiran 3bitr2i op1st2nd elima1c df-rex
-      snex bitr4i elxp2 opex elcompl dfral2 ralcom releqopab eqtr4i vvex ssetex
-      xpex swapex imageex txpex rnex difex ins2ex 1stex 2ndex inex si3ex ins4ex
-      1cex imaex complex eqeltri ) UAFFUBZGHZUCUDZHZUEZUFZGUGZGULZYKULZFUHHZUBZ
-      UIHZULZUJZUKZUMZUJZIUNZUJZIUNZUEZIUNZUOZUJZFUAAJZBJZCJZKZUUIUUHUUJKZVDZBD
-      JZLAUUNLZCDUPUUGABCDUQUUOCDUUFEJZUUJHZMZECURZVDZEUUNUUNUBZLZUUMAUUNLBUUNL
-      UUJUUNNZUUFMZUUOUUTUUMEBAUUNUUNUUPUUIUUHNZUSZUURUUKUUSUULUVFUURUVEUUQMZUU
-      KUUPUVEUUQUTUUKUUIUUHUUQKUVGUUIUUHUUJOUUIUUHUUQVAVEVBUVFUUSUVEUUJMUULUUPU
-      VEUUJUTUUIUUHUUJVAVBVCVFUVCUUEMZVGUUTVGZEUVAVHZVGUVDUVBUVHUVJUUPVIZUVCNUU
-      DMZERUUPUVAMZUVIPZERUVHUVJUVLUVNEUVLUVKUUJNZYJMZUVKUUNNZUUCMZPUVIUVMPUVNU
-      VKUUJUUNYJUUCVJUVPUVIUVRUVMUVPUVOYIMZUVOGMZVGZPUURUUSVGZPUVIUVOYIGVKUVSUU
-      RUWAUWBUUHUVOYHKZARUUHUUQUSZEAURZPZARUVSUURUWCUWFAUWCUUHUVKYEKZUUHUUJYGKZ
-      PUWEUWDPUWFUUHUVKUUJYEYGVLUWGUWEUWHUWDUWGUVKUUHGKUWEUUHUVKGOUUPUUHEVMZAVM
-      ZVNVOUUJUUHYFKUUHUCUUJUNZUSUWHUWDUUJUUHUCCVMZUWJWHUUHUUJYFOUUQUWKUUHUUJVP
-      VQQSUWEUWDVRTVSAUVOYHVTAUUPUUQUUJUWLWAWBQUVTUUSUUPUUJUWIUWLWCWDSUURUUSWET
-      UUHVIZUVQNZUUBMZARZUUPUUHUUINUSZBUUNVHZAUUNVHZUVRUVMUWPADURZUWRPZARUWSUWO
-      UXAAUWOUWNYKMZUWNUUAMZPUXAUWNYKUUAWFUXBUWTUXCUWRUXBUWMUUNNGMUWTUWMUVKUUNG
-      UUPWQZWGUUHUUNUWJDVMZWCVOUUIVIZUWNNZYTMZBRBDURZUWQPZBRUXCUWRUXHUXJBUXHUXG
-      YLMZUXGYSMZPUXJUXGYLYSWFUXKUXIUXLUWQUXKUXFUVQNYKMUXFUUNNGMUXIUXFUWMUVQYKU
-      UHWQWGUXFUVKUUNGUXDWGUUIUUNBVMZUXEWCTUXLUXFUWMUVKNNYRMUUIUUHUUPNZNZYQMZUW
-      QUXFUWMUVKUUNYRUXEWIUUIUUHUUPYQUXMUWJUWIWJUXPUXOYNMZUXOYPMZPUUPUUHUHKZUUP
-      UUIUIKZPUWQUXOYNYPWFUXQUXSUXRUXTUXQUXNYMMZUUHUUPYMKUXSUXQUUIFMUYAUXMUUIUX
-      NFYMWKWLUUHUUPYMVAUUHUUPUHOWMUXRUUIUUPNYOMUUIUUPYOKUXTUUIUUHUUPYOUWJWGUUI
-      UUPYOVAUUIUUPUIOWMSUUHUUIUUPUWJUXMWNTTSVOVSBUWNYTWOUWQBUUNWPQSVOVSUWRAUUN
-      WPWRAUVQUUBWOABUUPUUNUUNWSQSUVIUVMVRTVSEUVCUUDWOUVIEUVAWPQWDUVCUUEUUJUUNU
-      WLUXEWTXAUUTEUVAXBQUUMABUUNUUNXCQXDXEYDUUFFFXFXFXHUUEUUDIYJUUCYIGYHYEYGGX
-      GWAYFUCXIXJWAXKXLXGXMUUBIYKUUAGXGXNZYTIYLYSYKUYBXNYRYQYNYPFYMXFUHXOWAXHYO
-      UIXPWAXNXQXRXSXQXTYAXQXTYAXKXTYAYBXQYC $.
+      ( vx vy vr va vp csset cswap cin c1c cid cv cop wn vex wex otelins2 bitri
+      wcel wa anbi12i csym cins2 csi3 cins4 cima cdif ccompl cvv wbr wral copab
+      wi df-sym opex elcompl wrex csn wel elin opelssetsn 3bitri oqelins4 eldif
+      snex otsnelsi3 df-br brswap2 3bitr2i exbii elima1c df-clel 3bitr4i notbii
+      df-rex rexanali rexnal con2bii bitr4i opabbi2i eqtr4i ssetex ins2ex si3ex
+      wceq ideq swapex ins4ex inex 1cex imaex idex difex complex eqeltri ) UAFU
+      BZWOUBZGUCZUDZWPHZIUEZJUCZUDZWPHZIUEZUFZUDZHZIUEZHZIUEZUGZUHUAAKZBKZCKZUI
+      ZXMXLXNUIZULBDKZUJZAXQUJZCDUKXKABCDUMXSCDXKXNXQLZXKRXTXJRZMXSXTXJXNXQCNZD
+      NZUNUOYAXSYAXRMZAXQUPZXSMXLUQZXTLZXIRZAOADURZYDSZAOYAYEYHYJAYHYGWORZYGXHR
+      ZSYJYGWOXHUSYKYIYLYDYKYFXQLFRYIYFXNXQFYBPXLXQANZYCUTQYLXOXPMZSZBXQUPZYDXM
+      UQZYGLZXGRZBOBDURZYOSZBOYLYPYSUUABYSYRWPRZYRXFRZSUUAYRWPXFUSUUBYTUUCYOUUB
+      YQXTLWORYQXQLFRYTYQYFXTWOXLVDZPYQXNXQFYBPXMXQBNZYCUTVAUUCYQYFXNLZLZXERUUG
+      WTRZUUGXDRZMZSYOYQYFXNXQXEYCVBUUGWTXDVCUUHXOUUJYNEKZUQZUUGLZWSRZEOUUKXLXM
+      LZWDZECURZSZEOZUUHXOUUNUUREUUNUUMWRRZUUMWPRZSUURUUMWRWPUSUUTUUPUVAUUQUUTU
+      ULYQYFLLZWQRZUUPUULYQYFXNWQYBVBUVCUUKXMXLLZLZGRUUKUVDGUIUUPUUKXMXLGENZUUE
+      YMVEUUKUVDGVFUUKXMXLUUEYMVGVHQUVAUULUUFLWORUULXNLFRUUQUULYQUUFWOXMVDPUULY
+      FXNFUUDPUUKXNUVFYBUTVAZTQVIEUUGWSVJXOUUOXNRUUSXLXMXNVFEUUOXNVKQVLUUIXPUUM
+      XCRZEOUUKUVDWDZUUQSZEOZUUIXPUVHUVJEUVHUUMXBRZUVASUVJUUMXBWPUSUVLUVIUVAUUQ
+      UVLUVBXARZUVIUULYQYFXNXAYBVBUVMUVEJRUUKUVDJUIUVIUUKXMXLJUVFUUEYMVEUUKUVDJ
+      VFUUKUVDXMXLUUEYMUNWEVHQUVGTQVIEUUGXCVJXPUVDXNRUVKXMXLXNVFEUVDXNVKQVLVMTV
+      ATQVIBYGXGVJYOBXQVNVLXOXPBXQVOQTQVIAXTXIVJYDAXQVNVLXRAXQVPQVQVRVSVTXJXIIW
+      OXHFWAWBZXGIWPXFWOUVNWBZXEWTXDWSIWRWPWQGWFWCWGUVOWHWIWJXCIXBWPXAJWKWCWGUV
+      OWHWIWJWLWGWHWIWJWHWIWJWMWN $.
   $}
 
   $( The class of all partial orderings is a set.  (Contributed by SF,
@@ -57809,16 +57786,17 @@ the first case of his notation (simple exponentiation) and subscript it
     $( The equinumerosity relationship is a set.  (Contributed by SF,
        23-Feb-2015.) $)
     enex $p |- ~~ e. _V $=
-      ( vx vy vf vg cen cvv cfns cswap ccnv ctxp crn cv wex cop wcel wbr wa wfn
-      elrn bitri cxp cimage cin wf1o copab df-en brfns wceq df-br trtxp brimage
-      cima brcnv dfcnv2 eqeq2i 3bitr4i anbi12i exbii cnvex fneq1 ceqsexv dff1o4
-      releqopab eqtr4i vvex xpex fnsex swapex imageex txpex rnex inex eqeltri
-      vex ) EFFUAZGHUBZIZGJZKZJZKZUCZFEALZBLZCLZUDZCMZABUEWBABCUFWGABWAWCWDNZWA
-      OWEWHVTPZCMWGCWHVTSWIWFCWEWCGPZWEWDVSPZQWEWCRZWEIZWDRZQWIWFWJWLWKWNWCWECV
-      NZUGWKDLZWMUHZWPWDRZQZDMZWNWKWEWDNZVSOZWTWEWDVSUIXBWPXAVRPZDMWTDXAVRSXCWS
-      DXCWPWEVQPZWPWDGPZQWSWPWEWDVQGUJXDWQXEWRWEWPVPPWPHWEULZUHXDWQWEWPHWODVNZU
-      KWPWEVPUMWMXFWPWEUNUOUPWDWPXGUGUQTURTTWRWNDWMWEWOUSWDWPWMUTVATUQWEWCWDGVS
-      UJWCWDWEVBUPURTVCVDVOWAFFVEVEVFVTGVSVGVRVQGVPHVHVIUSVGVJVKVJVKVLVM $.
+      ( vx vy vf vg cen cfns cswap ccnv ctxp crn cv wex cop wcel elrn2 wa df-br
+      wfn wbr bitri cimage cvv wf1o copab df-en vex bitr3i wceq oteltxp opelcnv
+      brfns cima dfcnv2 eqeq2i brimage anbi12i exbii cnvex fneq1 ceqsexv dff1o4
+      3bitr2ri 3bitr4i opabbi2i eqtr4i fnsex swapex imageex txpex rnex eqeltri
+      ) EFGUAZHZFIZJZIZJZUBEAKZBKZCKZUCZCLZABUDVQABCUEWBABVQVRVSMZVQNVTWCMVPNZC
+      LWBCWCVPOWDWACVTVRMFNZVTVSMZVONZPVTVRRZVTHZVSRZPWDWAWEWHWGWJWEVTVRFSWHVTV
+      RFQVRVTCUFZUKUGWGDKZWFMVNNZDLZWJDWFVNOWNWLWIUHZWLVSRZPZDLWJWMWQDWMWLVTMVM
+      NZWLVSMFNZPWQWLVTVSVMFUIWRWOWSWPWRVTWLMVLNZWOWLVTVLUJWOWLGVTULZUHVTWLVLSW
+      TWIXAWLVTUMUNVTWLGWKDUFZUOVTWLVLQVBTWSWLVSFSWPWLVSFQVSWLXBUKUGUPTUQWPWJDW
+      IVTWKURVSWLWIUSUTTTUPVTVRVSFVOUIVRVSVTVAVCUQTVDVEVPFVOVFVNVMFVLGVGVHURVFV
+      IVJVIVJVK $.
   $}
 
   ${
@@ -58210,22 +58188,22 @@ the first case of his notation (simple exponentiation) and subscript it
     $( Lemma for ~ enpw1 .  Set up stratification for the reverse direction.
        (Contributed by SF, 26-Feb-2015.) $)
     enpw1lem1 $p |- { <. x , y >. | { x } g { y } } e. _V $=
-      ( vp va vb cvv c1st c2nd cv csn wbr wceq wa wex ancom 3bitri anbi1i bitri
-      weq cxp ccnv csi ccom cin cima cuni1 copab cop wcel wrex vex eluni1 elima
-      opex brin brco brsnsi2 brcnv opbr1st equcom exbii sneq ceqsexv snex breq2
-      eqeq2d opbr2nd anbi12i op1st2nd rexbii df-br risset bitr2i releqopab vvex
-      xpex 1stex cnvex siex coex 2ndex inex imaex uni1ex eqeltrri ) GGUAZHUBZUC
-      ZHUDZIUBZUCZIUDZUEZCJZUFZUGZUEAJZKZBJZKZWOLZABUHGXBABWQWRWTUIZWQUJXCKZWPU
-      JZDJZWSXAUIZMZDWOUKZXBXCWPWRWTAULZBULZUOZUMXEXFXDWNLZDWOUKXIDXDWNWOUNXMXH
-      DWOXMXFXDWJLZXFXDWMLZNXFWSHLZXFXAILZNXHXFXDWJWMUPXNXPXOXQXNXFEJZHLZXRXDWI
-      LZNZEOXRWSMZXSNZEOXPEXFXDWIHUQYAYCEYAXTXSNYCXSXTPXTYBXSXTXRFJZKZMZYDXCWHL
-      ZNZFOFATZYFNZFOYBFXCXRWHXLURYHYJFYHYGYFNYJYFYGPYGYIYFYGXCYDHLAFTYIYDXCHUS
-      WRWTYDXJXKUTAFVAQRSVBYFYBFWRXJYIYEWSXRYDWRVCVGVDQRSVBXSXPEWSWRVEZXRWSXFHV
-      FVDQXOXFXRILZXRXDWLLZNZEOXRXAMZYLNZEOXQEXFXDWLIUQYNYPEYNYMYLNYPYLYMPYMYOY
-      LYMYFYDXCWKLZNZFOFBTZYFNZFOYOFXCXRWKXLURYRYTFYRYQYFNYTYFYQPYQYSYFYQXCYDIL
-      BFTYSYDXCIUSWRWTYDXJXKVHBFVAQRSVBYFYOFWTXKYSYEXAXRYDWTVCVGVDQRSVBYLXQEXAW
-      TVEZXRXAXFIVFVDQVIWSXAXFYKUUAVJQVKSXBXGWOUJXIWSXAWOVLDXGWOVMVNQVOWGWQGGVP
-      VPVQWPWNWOWJWMWIHWHHVRVSVTVRWAWLIWKIWBVSVTWBWAWCCULWDWEWCWF $.
+      ( vp va vb c1st c2nd cv csn wbr wceq wa wex ancom weq bitri exbii ceqsexv
+      3bitri ccnv csi ccom cin cima cuni1 copab cvv wcel wrex opex eluni1 elima
+      cop vex brin brco brsnsi2 brcnv opbr1st equcom anbi1i sneq eqeq2d opbr2nd
+      snex breq2 anbi2i anbi12i op1st2nd rexbii df-br risset bitr2i 1stex cnvex
+      opabbi2i siex coex 2ndex inex imaex uni1ex eqeltrri ) GUAZUBZGUCZHUAZUBZH
+      UCZUDZCIZUEZUFZAIZJZBIZJZWLKZABUGUHWSABWNWOWQUNZWNUIWTJZWMUIZDIZWPWRUNZLZ
+      DWLUJZWSWTWMWOWQAUOZBUOZUKZULXBXCXAWKKZDWLUJXFDXAWKWLUMXJXEDWLXJXCXAWGKZX
+      CXAWJKZMXCWPGKZXCWRHKZMXEXCXAWGWJUPXKXMXLXNXKXCEIZGKZXOXAWFKZMZENXOWPLZXP
+      MZENXMEXCXAWFGUQXRXTEXRXQXPMXTXPXQOXQXSXPXQXOFIZJZLZYAWTWEKZMZFNFAPZYCMZF
+      NXSFWTXOWEXIURYEYGFYEYDYCMYGYCYDOYDYFYCYDWTYAGKAFPYFYAWTGUSWOWQYAXGXHUTAF
+      VATVBQRYCXSFWOXGYFYBWPXOYAWOVCVDSTVBQRXPXMEWPWOVFZXOWPXCGVGSTXLXCXOHKZXOX
+      AWIKZMZENXOWRLZYIMZENXNEXCXAWIHUQYKYMEYKYIYLMYMYJYLYIYJYCYAWTWHKZMZFNFBPZ
+      YCMZFNYLFWTXOWHXIURYOYQFYOYCYPMYQYNYPYCYNWTYAHKBFPYPYAWTHUSWOWQYAXGXHVEBF
+      VATVHYCYPOQRYCYLFWQXHYPYBWRXOYAWQVCVDSTVHYIYLOQRYIXNEWRWQVFZXOWRXCHVGSTVI
+      WPWRXCYHYRVJTVKQWSXDWLUIXFWPWRWLVLDXDWLVMVNTVQWMWKWLWGWJWFGWEGVOVPVRVOVSW
+      IHWHHVTVPVRVTVSWACUOWBWCWD $.
   $}
 
   ${
@@ -61539,18 +61517,17 @@ the first case of his notation (simple exponentiation) and subscript it
        relationship.  (Contributed by SF, 6-Mar-2015.) $)
     spacvallem1 $p |- { <. x , y >. | ( x e. NC /\ y e. NC /\ y = ( 2c ^c x
         ) ) } e. _V $=
-      ( vt cvv cxp cncs cce c2nd c1st ccnv c2c cin wcel wceq cop wbr wex 3bitri
-      cv wa cfullfun cima cres ccom co copab opelxp opelco brcnv brres eliniseg
-      csn w3a anbi2i ancom 2nc elexi vex op1st2nd anbi1i exbii bitri opex breq1
-      ceqsexv brfullfunop eqcom anbi12i elin df-3an 3bitr4i releqopab vvex xpex
-      ncsex ceex fullfunex 2ndex 1stex cnvex snex imaex resex coex eqeltrri
-      inex ) DDEZFFEZGUAZHIJZKULZUBZUCZJZUDZLZLASZFMZBSZFMZWSKWQGUEZNZUMZABUFDX
-      CABWPWQWSOZWHMZXDWOMZTWRWTTZXBTXDWPMXCXEXGXFXBWQWSFFUGXFCSZKWQOZNZXHWSWIP
-      ZTZCQZXIWSWIPZXBXFWQXHWNPZXKTZCQXMCWQWSWIWNUHXPXLCXOXJXKXOXHWQWMPZXHKIPZX
-      HWQHPZTZXJWQXHWMUIXQXSXHWLMZTXSXRTXTXHWQHWLUJYAXRXSIKXHUKUNXSXRUORKWQXHKF
-      UPUQZAURZUSRUTVAVBXKXNCXIKWQYBYCVCXHXIWSWIVDVEXNXAWSNXBKWQWSGYBYCVFXAWSVG
-      VBRVHXDWHWOVIWRWTXBVJVKVLWGWPDDVMVMVNWHWOFFVOVOVNWIWNGVPVQWMHWLVRWJWKIVSV
-      TKWAWBWCVTWDWFWFWE $.
+      ( vt cncs cce c2nd c1st ccnv c2c cv wcel wceq cop wa wbr wex anbi1i bitri
+      3bitri ncsex cxp cfullfun csn cima cres ccom cin co w3a cvv opelxp opelco
+      copab brcnv brres ancom eliniseg 2nc elexi vex op1st2nd exbii brfullfunop
+      opex breq1 ceqsexv eqcom anbi12i elin df-3an opabbi2i xpex ceex fullfunex
+      3bitr4i 2ndex 1stex cnvex snex imaex resex coex inex eqeltrri ) DDUAZEUBZ
+      FGHZIUCZUDZUEZHZUFZUGZAJZDKZBJZDKZWPIWNEUHZLZUIZABUMUJWTABWMWNWPMZWEKZXAW
+      LKZNWOWQNZWSNXAWMKWTXBXDXCWSWNWPDDUKXCCJZIWNMZLZXEWPWFOZNZCPZXFWPWFOZWSXC
+      WNXEWKOZXHNZCPXJCWNWPWFWKULXMXICXLXGXHXLXEWNWJOZXEIGOZXEWNFOZNZXGWNXEWJUN
+      XNXPXEWIKZNXRXPNXQXEWNFWIUOXPXRUPXRXOXPGIXEUQQSIWNXEIDURUSZAUTZVASQVBRXHX
+      KCXFIWNXSXTVDXEXFWPWFVEVFXKWRWPLWSIWNWPEXSXTVCWRWPVGRSVHXAWEWLVIWOWQWSVJV
+      OVKWEWLDDTTVLWFWKEVMVNWJFWIVPWGWHGVQVRIVSVTWAVRWBWCWD $.
   $}
 
   ${