[prove] upeu2

Author: zwang123

set.mm

@@ -835706,6 +835706,12 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     $}
 
     ${
+      $d B g l p $.  $d B w $.  $d D l p $.  $d E p $.  $d F f k w $.
+      $d F l p $.  $d G f k w $.  $d G l p $.  $d H f k w $.  $d H l p $.
+      $d I p $.  $d J f w $.  $d J l p $.  $d K l p $.  $d M f k w $.
+      $d M l p $.  $d N p $.  $d O f k w $.  $d O l p $.  $d X f k w $.
+      $d X l p $.  $d Y l p $.  $d Z f k w $.  $d Z l p $.  $d f g k p v $.
+      $d g l p ph v $.  $d p v w $.
       upeu2.i $e |- I = ( Iso ` D ) $.
       upeu2.k $e |- ( ph -> K e. ( X I Y ) ) $.
       upeu2.n $e |- ( ph ->
@@ -835717,7 +835723,24 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
            E! l e. ( Y H v )
            g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) )
       $=
-        (  ) ? $.
+        ( vp cfv co wcel cv cop wceq wreu wral funcrcl3 funcf1 ffvelcdmd funcf2
+        funcrcl2 isohom sseldd catcocl eqeltrd wa adantr simprl simprr cco eqid
+        upciclem1 ccat ad2antrr simpr upeu2lem fveq2d cfunc wbr upciclem2 eqtrd
+        oveq1d eqeq2d reuxfr1dd mpbid ralrimivva jca ) ARUBUAKUSZOUTZVAHVBZUCVB
+        ZUACVBZLUTUSRUBWRVCXBKUSZSUTUTZVDZUCUAXBMUTZVEZHUBXCOUTZVFCDVFARPTUALUT
+        ZUSZQUBTKUSZVCZWRSUTUTZWSUQAEJSQXJOUBXKWRUEUGUHAFJKLUIVGULADETKADEFJKLU
+        DUEUIVHZUJVIADEUAKXNUKVIUMATUAMUTZXKWROUTPXIADFJKLMOTUAUDUFUGUIUJUKVJAT
+        UANUTZXOPADFMNTUAUDUFUOAFJKLUIVKZUJUKVLUPVMZVIVNVOAXGCHDXHAXBDVAZWTXHVA
+        ZVPZVPZWTURVBZTXBLUTZUSZQXLXCSUTZUTZVDZURTXBMUTZVEXGYBBDIGKLMOQWTSTXBUB
+        URAGVBIVBTBVBZLUTUSQXLYJKUSZSUTUTVDITYJMUTVEGUBYKOUTVFBDVFYAUNVQAXSXTVR
+        ZAXSXTVSWBYBYHXEURUCXAPTUAVCXBFVTUSZUTUTZYIXFYBXAXFVAZVPDFYMPXAMTUAXBUD
+        UFYMWAZAFWCVAZYAYOXQWDATDVAZYAYOUJWDAUADVAZYAYOUKWDYBXSYOYLVQAPXOVAZYAY
+        OXRWDYBYOWEVNYBYCYIVAZVPDFYMUCPYCMNTUAXBUDUFYPUOAYQYAUUAXQWDAYRYAUUAUJW
+        DAYSYAUUAUKWDYBXSUUAYLVQAPXPVAYAUUAUPWDYBUUAWEWFYBYOYCYNVDZVPZVPZYGXDWT
+        UUDYGYNYDUSZQYFUTXDUUDYEUUEQYFUUDYCYNYDYBYOUUBVSWGWLUUDDEFYMJKLMOPXAQRS
+        UBTUAXBUDUEUFUGUHAKLFJWHUTWIYAUUCUIWDAYRYAUUCUJWDAYSYAUUCUKWDYBXSUUCYLV
+        QAUBEVAYAUUCULWDAQUBXKOUTVAYAUUCUMWDYPAYTYAUUCXRWDYBYOUUBVRARXMVDYAUUCU
+        QWDWJWKWMWNWOWPWQ $.
     $}
   $}