Hi Norm,
There are 598 out of 5398 theorems (6/26/2006 set.mm) with the weq, wel,wsb problem. I believe these are the steps involved – 2078 proof steps. List enclosed below… All remaining theorems are satisfactorily unified (without being told the Ref label on each step, I might add.)
Notice that opeq2 is used by fcoi2 but both of these are class only assertions! So, inside the proofs they descend to the set variable level even though then end result is all class variables. Hmmm.
My problem with "DisableGrammarRule?" is that wcel, etc. are defined much later than wel etc. So the intervening statements fail in the parse step. And, if I try moving wcel to be right after wel that seems to cause problems in existing proofs because the order of hypotheses changes.
And, hardcoding for weq, wel, and wsb is problematic because I don't know exactly when to do it! I cannot do it all the time because weq has its own uses, and so I almost have to wait for unification failure before trying to do fix-up on the parse tree, and how do I know that the error is not caused by something else, like a user error.
So this is the old ambiguity problem again – set.mm requires two different parse trees for a given expression, depending on the context of its use. It wants "x = y" to be considered as "set = set" in the formula the user sees, but the proof may need it parsed as either "class = class" or "set = set", depending on which theorem is used as justification.
It seems as if there ought to be a way to create alternate proofs that don't run into this problem – alternate set only versions of assertions such as eleq1, opeq2, etc. But there are 317!
I'm about ready to declare victory and withdraw my troops on this one, and document the "feature" that the mmj2 GUI Proof Assistant cannot unify conflicting overloaded operators.
"Ref","Theorem","Step","ID"
"eleq1","cleqf","6",1
"eleq1","cleqf","7",2
"eleq1","hblem","2",3
"eleq1","hblem","3",4
"hbeq","hbel","4",5
"hbel","hbeleq","4",6
"hbeq","hbeleq","qed",7
"eqeq1","clelab","9",8
"hbel","sbabel","5",9
"eqab","sbabel","18",10
"eqab","sbabel","20",11
"eleq1","rgen2","5",12
"eleq1","rgen2","15",13
"hbel","hbrab","4",14
"eleq1","ralcom2","3",15
"eleq1","ralcom2","9",16
"eleq1","ralcom2","19",17
"eleq1","ralcom2","28",18
"eleq1","cbvralf","12",19
"eleq1","cbvrex","8",20
"eleq1","cbvreuv","4",21
"eleq1","reu2","10",22
"eqid","visset","1",23
"eqeq1","vtoclgf","9",24
"eqeq1","cla4gf","8",25
"eqeq2","eqvinc","10",26
"eqeq1","eqvinc","13",27
"eqeq1","eqvinc","14",28
"eqeq1","eqvincf","9",29
"eqeq1","eqvincf","10",30
"eqeq2","alexeq","2",31
"eqeq2","alexeq","5",32
"eqeq2","ceqex","4",33
"eqeq2","ceqex","5",34
"alexeq","ceqex","15",35
"elabf","cbvab","8",36
"hbel","cbvrab","7",37
"hbel","cbvrab","10",38
"eleq1","cbvrab","12",39
"eqtr3t","eueq","1",40
"eqeq1","eueq","5",41
"eqeq2","moeq3","4",42
"eueq3","moeq3","11",43
"eueq3","moeq3","16",44
"eqeq2","mo2icl","1",45
"eleq1","ru","2",46
"eleq12d","ru","5",47
"df-nel","ru","7",48
"eqab","ru","12",49
"eqeq1","vsbcint","3",50
"ceqsexv","vsbcint","4",51
"raleq","sbralie","8",52
"dfsbcq","sbceq1","1",53
"dfsbcq","a4sbc","1",54
"dfsbcq","hbsbcg","2",55
"hbeq","hbsbcg","4",56
"dfsbcq","hbsbcg","5",57
"dfsbcq","sbcco","1",58
"dfsbcq","sbcco","2",59
"eqcom","sbcco2","3",60
"dfsbcq","sbcn","1",61
"dfsbcq","sbcn","2",62
"dfsbcq","sbcim","1",63
"dfsbcq","sbcim","2",64
"dfsbcq","sbcim","3",65
"dfsbcq","sbcan","1",66
"dfsbcq","sbcan","2",67
"dfsbcq","sbcan","3",68
"dfsbcq","sbcor","1",69
"dfsbcq","sbcor","2",70
"dfsbcq","sbcor","3",71
"dfsbcq","sbcbi","1",72
"dfsbcq","sbcbi","2",73
"dfsbcq","sbcbi","3",74
"dfsbcq","sbcal","1",75
"dfsbcq","sbcal","2",76
"dfsbcq","sbcex","1",77
"dfsbcq","sbcex","2",78
"eleq2","axrep","2",79
"eleq2","axrep","27",80
"vtocl","axrep","32",81
"vtoclf","axrep2","qed",82
"hbeq","zfrepclf","5",83
"eleq2","zfrepclf","6",84
"hbeq","zfrepclf","13",85
"eleq2","zfrepclf","14",86
"eqab","zfrep4","11",87
"eleq1","zfaus","15",88
"ceqsexv","zfaus","17",89
"zfaus","bm1.3ii","8",90
"zfaus","nalset","3",91
"dfcleq","nvelv","5",92
"eleq1","dfss2f","6",93
"eleq1","dfss2f","7",94
"dfcleq","inex1","3",95
"eqid","dfnul2","4",96
"eqid","dfnul3","2",97
"eqid","noel","1",98
"eleq1","abn0","4",99
"eq0","0el","2",100
"zfaus","zfnul","2",101
"hbel","hbif","5",102
"hbel","hbif","8",103
"hbel","hbpw","4",104
"hbss","hbpw","5",105
"dfss2","pwex","5",106
"eqab","pwex","13",107
"eleq2","el","4",108
"eleq2","rext","4",109
"eleq2","rext","5",110
"elsn","rext","9",111
"df-sn","moabex","3",112
"elsn","exss","20",113
"dfss2","pwpw0","1",114
"n0","pwpw0","7",115
"df-clel","pwpw0","8",116
"eqeq2","dtru","3",117
"eqeq2","dtru","8",118
"eqcom","dtru","13",119
"dfpr2","zfpair","1",120
"opth","copsexg","8",121
"ceqex","copsexg","10",122
"ceqex","copsexg","11",123
"opth","copsexg","18",124
"opth2","moop2","4",125
"hbop","moop2","11",126
"opeq2","moop2","16",127
"elsn","eusn","2",128
"sneq","eusn","11",129
"eleq1","eluni","5",130
"hbel","hbuni","4",131
"eluni","hbuni","7",132
"eluni","hbuni","8",133
"eleq2","eluniab","6",134
"eleq1","eluniab","7",135
"clel3","unpr","10",136
"clel3","unpr","13",137
"eluni","uniun","7",138
"eluni","uniun","8",139
"eluni","uniun","11",140
"eluni","uniin","2",141
"eluni","uniin","10",142
"eluni","uniin","11",143
"eluni","ssuni","5",144
"dfss2","ssuni","9",145
"n0","uni0b","6",146
"eluni2","uni0b","8",147
"eluni","unissb","2",148
"dfss2","unissb","13",149
"sseq1","unisseq","6",150
"elrab","unisseq","7",151
"eluni","uniex","5",152
"dfcleq","uniex","11",153
"hbeq","euuni","10",154
"eqeq2","euuni","12",155
"eluni","unipw","1",156
"ssel","unipw","4",157
"eleq2","unipw","13",158
"eluni","unipw","20",159
"eleq1","elint","2",160
"eleq1","elintg","2",161
"elint2","elintg","6",162
"eleq1","elinti","1",163
"elint","elinti","5",164
"hbel","hbint","3",165
"elint","hbint","8",166
"elint","hbint","10",167
"eleq1","elintab","7",168
"eleq2","elintab","10",169
"eqid","int0","4",170
"eleq2","intss1","2",171
"elint","intss1","7",172
"elint2","ssint","3",173
"dfss3","ssint","6",174
"sseq2","ssintub","2",175
"elrab","ssintub","3",176
"eleq2","intmin","3",177
"elintrab","intmin","8",178
"elint","intss","4",179
"elint","intss","6",180
"elint","intun","8",181
"elint","intun","10",182
"elint","intun","14",183
"clel4","intpr","10",184
"clel4","intpr","11",185
"elint","intpr","15",186
"clel3","dfiun2","3",187
"eqeq1","dfiun2","16",188
"elab","dfiun2","18",189
"clel4","dfiin2","3",190
"eqeq1","dfiin2","15",191
"elab","dfiin2","17",192
"elrabsf","iunrab","13",193
"df-iun","uniiun","2",194
"df-iin","intiin","2",195
"elun","iinuni","2",196
"elint2","iinuni","5",197
"elun","iununi","13",198
"eluni2","iununi","17",199
"eluni","iununi","24",200
"eluni","dftr2","4",201
"df-ral","dftr5","5",202
"eleq2","trel","6",203
"breq1","brab1","2",204
"elab","brab1","3",205
"opth","opabid","13",206
"opeq1","opabid","30",207
"opeq2","opabid","40",208
"eqid","biopabi","2",209
"opeq12","cbvopab","14",210
"opeq1","cbvopab1","10",211
"opeq1","cbvopab1s","6",212
"opeq1","cbvopab1v","2",213
"opeq2","cbvopab2v","2",214
"opeq12","opabsb","16",215
"eleq1","epelc","3",216
"epelc","epel","qed",217
"eqeq1","ideqg","1",218
"eqeq1","solin","2",219
"eqid","so","2",220
"eleq1","so","5",221
"eqeq2","so","7",222
"breq1","so","8",223
"breq2","so","10",224
"eleq1","so","20",225
"eleq1","so","37",226
"eleq1","supmo","2",227
"breq1","supmo","3",228
"breq2","supmo","6",229
"breq1","supmo","12",230
"breq1","supmo","13",231
"rcla4v","supmo","16",232
"breq2","supmo","20",233
"breq1","supmo","30",234
"breq1","supmo","31",235
"rcla4v","supmo","34",236
"breq2","supmo","38",237
"sotrieq2","supmo","49",238
"breq2","supub","5",239
"rcla4v","supub","7",240
"breq1","suplub","7",241
"breq1","suplub","8",242
"rcla4v","suplub","11",243
"breq1","dffr2","4",244
"elab","dffr2","5",245
"breq2","dffr2","10",246
"elsn","frirr","10",247
"breq2","frirr","11",248
"breq1","frirr","16",249
"elab","frirr","17",250
"breq2","fr2nr","5",251
"breq2","fr2nr","18",252
"elpr","fr2nr","33",253
"breq2","fr3nr","6",254
"breq2","fr3nr","19",255
"breq2","fr3nr","32",256
"eltp","fr3nr","47",257
"eleq1","efrirr","2",258
"frirr","efrirr","7",259
"abid2","dfepfr","4",260
"abid2","epfrc","6",261
"solin","dfwe2","2",262
"breq2","dfwe2","10",263
"breq2","dfwe2","45",264
"eqeq2","dfwe2","46",265
"breq1","dfwe2","47",266
"solin","wecmpep","1",267
"ineq2","wefrc","2",268
"rcla4ev","wefrc","4",269
"elin","wefrc","15",270
"elin","wefrc","32",271
"dfss3","wefrc","37",272
"solin","wereu","5",273
"breq1","wereu","18",274
"rcla4v","wereu","20",275
"breq1","wereu","21",276
"rcla4v","wereu","23",277
"breq2","wereu","35",278
"trel3","ordelord","11",279
"trel","ordelord","20",280
"dftr2","ordelord","33",281
"eleq1","tz7.7","25",282
"trel","tz7.7","32",283
"ssrdv","tz7.7","46",284
"ineq2","onfr","2",285
"rcla4ev","onfr","4",286
"ssel","onfr","7",287
"sseli","onfr","20",288
"trss","onfr","21",289
"sseli","onfr","23",290
"ra4e","onfr","39",291
"n0","onfr","50",292
"ordelord","ordon","3",293
"ssrdv","ordon","11",294
"ordtri3or","ordon","15",295
"hbral","tfis","6",296
"eleq1","tfis","10",297
"raleq","tfis","11",298
"elrabsf","tfis","18",299
"elrabsf","tfis","25",300
"trss","ssorduni","8",301
"eluni2","ssorduni","16",302
"ordelord","ssorduni","23",303
"eluni2","ssorduni","31",304
"sseq2","ordunidif","24",305
"rcla4ev","ordunidif","25",306
"ontri1","onint","2",307
"ssel","onint","3",308
"disj","onint","10",309
"elint2","onint","12",310
"ssrdv","onint","20",311
"eleq2","onminex","15",312
"eleq1","onminex","31",313
"elab","onminex","33",314
"df-ral","onminex","46",315
"dfcleq","sucel","2",316
"eluni2","unon","1",317
"onelon","unon","2",318
"limeq","limuni2","1",319
"rcla4v","limuni2","2",320
"limeq","limuni2","12",321
"rcla4v","limuni2","13",322
"limeq","limuni2","22",323
"rcla4v","limuni2","23",324
"limsuc","limuni2","25",325
"eluni2","limuni2","33",326
"ontri1","dfom2","5",327
"limeq","dfom2","8",328
"elrab","dfom2","10",329
"eleq1","elom","3",330
"eleq1","elomg","3",331
"elom","elomg","8",332
"elom","omsson","2",333
"eleq2","limomss","4",334
"elom","limomss","8",335
"ordelord","ordom","2",336
"trel","ordom","6",337
"elom","ordom","16",338
"elom","ordom","22",339
"limeq","omssnlim","4",340
"elrab","omssnlim","6",341
"eleq2","peano5","22",342
"minel","peano5","28",343
"elab","finds","11",344
"sseq2","findsg","22",345
"elab","finds2","13",346
"dfsbcq","findes","3",347
"dfsbcq","findes","5",348
"eleq1","findes","14",349
"suceq","findes","16",350
"finds","findes","qed",351
"rcla4v","tfinds","44",352
"sseq2","tfindsg","23",353
"onelon","tfindsg2","33",354
"biraldva","tfindsg2","39",355
"dfsbcq","tfindes","4",356
"dfsbcq","tfindes","6",357
"eleq1","tfindes","15",358
"suceq","tfindes","17",359
"tfinds","tfindes","qed",360
"sbcel1","tfinds2","14",361
"sbcie","tfinds2","22",362
"suceq","tfinds2","28",363
"limeq","tfinds2","37",364
"hbel","hbxp","5",365
"hbel","hbxp","7",366
"opth","opelxp","12",367
"df-clel","opelxp","24",368
"ssel","weinxp","1",369
"ssel","weinxp","2",370
"biraldva","weinxp","11",371
"birexdva","weinxp","12",372
"eluni2","reluni","2",373
"dfss2","reluni","7",374
"hbbr","hbco","5",375
"hbbr","hbco","8",376
"hbbr","hbcnv","5",377
"opeq2","dfdmf","7",378
"opeq1","dfdmf","15",379
"eqid","dm0","3",380
"eqid","dmsn0","6",381
"eqid","dmsnsn0","12",382
"ideq","dmi","4",383
"eqcom","dmi","5",384
"eqid","dmi","9",385
"opeq1","dfrnf","7",386
"opeq2","dfrnf","15",387
"hbel","hbrn","4",388
"ideq","iss","5",389
"ideq","iss","13",390
"eqcom","iss","17",391
"opeq2","iss","22",392
"ceqsexv","iss","24",393
"opeq2","iss","30",394
"ideq","iss","40",395
"hbel","hbima","4",396
"hbop","hbima","7",397
"ideq","imai","5",398
"eleq1","imai","12",399
"ceqsexv","imai","13",400
"ideq","intasym","18",401
"opeq2","intirr","10",402
"ceqsexv","intirr","12",403
"ideq","intirr","19",404
"eqcom","intirr","21",405
"opeq1","cnvopab","13",406
"opeq2","cnvopab","15",407
"opeq2","cnvopab","25",408
"opeq1","cnvopab","27",409
"eqcom","cnvi","3",410
"ideq","cnvi","7",411
"ideq","cnvi","15",412
"eluni","imaiun","1",413
"elima3","imaiun","15",414
"ideq","coi1","7",415
"eqcom","coi1","8",416
"breq1","coi1","13",417
"ceqsexv","coi1","14",418
"breq12d","cnvpo","20",419
"eqcom","cnvso","6",420
"breq2","dffun3","2",421
"hbbr","dffunmof","6",422
"breq2","dffunmof","8",423
"hbbr","dffunmof","16",424
"breq1","dffunmof","20",425
"eqtr3t","funsn","5",426
"funeq","fununi","32",427
"sseq1","fununi","33",428
"sseq2","fununi","34",429
"sseq2","fununi","37",430
"sseq1","fununi","38",431
"sseq1","fununi","43",432
"sseq2","fununi","44",433
"funeq","fununi","49",434
"sseq2","fununi","50",435
"sseq1","fununi","51",436
"cnveq","funcnvuni","1",437
"sseq1","funcnvuni","4",438
"sseq2","funcnvuni","5",439
"rcla4v","funcnvuni","9",440
"sseq2","funcnvuni","13",441
"sseq1","funcnvuni","14",442
"rcla4v","funcnvuni","16",443
"cnveq","funcnvuni","35",444
"eqeq1","funcnvuni","42",445
"elab","funcnvuni","44",446
"eqeq1","funcnvuni","47",447
"elab","funcnvuni","49",448
"dfima3","funimaexg","9",449
"eqab","funimaexg","11",450
"rexeqf","zfrep6","9",451
"df-rab","zfrep6","21",452
"df-ral","zfrep6","31",453
"df-rab","zfrep6","43",454
"eleq2d","zfrep6","46",455
"r19.21ai","zfrep6","60",456
"opeq2","fnopabg","38",457
"ideq","fcoi1","15",458
"eqcom","fcoi1","17",459
"opeq1","fcoi1","26",460
"ceqsexv","fcoi1","29",461
"ideq","fcoi2","16",462
"opeq2","fcoi2","25",463
"eleq1","fcoi2","27",464
"ceqsexv","fcoi2","29",465
"elsn","fv2","14",466
"elfv","fv3","2",467
"breq2","fv3","6",468
"ceqsalv","fv3","7",469
"eleq2","fv3","11",470
"breq2","fv3","12",471
"eqrd","tz6.12-1","qed",472
"opeq2","tz6.12f","3",473
"opeq2","tz6.12f","8",474
"eqeq2","tz6.12f","13",475
"elab","tz6.12-2","5",476
"eleq1","fnopabfv","15",477
"fveq2","fnopabfv","16",478
"eqeq1","fnopabfv","19",479
"opelopab","fnopabfv","21",480
"eqeq1","fvopabn","13",481
"opelopabg","fvopabn","14",482
"eqvincf","fvopabgf","6",483
"eqeqan12rd","fvopabgf","24",484
"eqvincf","fvopabnf","6",485
"eqeqan12rd","fvopabnf","24",486
"hbfv","fvopab2","5",487
"hbfv","cleqfvf","5",488
"hbfv","cleqfvf","7",489
"fveq2","cleqfvf","10",490
"fveq2","cleqfvf","11",491
"hbfv","elrnopab","13",492
"fveq2","elrnopab","17",493
"eleq1","chfnrn","5",494
"eluni2","chfnrn","10",495
"opeq1","fvrn","8",496
"cla4ev","fvrn","10",497
"eqid","fvi","9",498
"ideq","fvi","12",499
"fveq2","fconstfv","17",500
"rcla4v","fconstfv","19",501
"fveq2","fvresex","4",502
"fvopab","fvresex","5",503
"hbfv","abrexexlem2","17",504
"hbeq","abrexexlem2","18",505
"fveq2","abrexexlem2","19",506
"hbfv","abrexexlem2","29",507
"hbeq","abrexexlem2","30",508
"eqeq1","abrexexlem2","32",509
"breq1","f1fv","45",510
"hbfv","f1fvf","5",511
"hbfv","f1fvf","7",512
"fveq2","f1fvf","14",513
"eqeq2","f1fvf","16",514
"hbfv","f1fvf","22",515
"hbfv","f1fvf","24",516
"fveq2","f1fvf","30",517
"eqeq1","f1fvf","32",518
"eqeq1","f1fveq","3",519
"hbel","hbiso","8",520
"hbel","hbiso","10",521
"hbbr","hbiso","13",522
"hbfv","hbiso","15",523
"hbfv","hbiso","17",524
"breq1","isotr","28",525
"fveq2","isotr","29",526
"breq2","isotr","32",527
"fveq2","isotr","33",528
"rcla42v","isotr","36",529
"ssel","isofrlem","20",530
"funfvima","isofrlem","21",531
"n0","isofrlem","29",532
"ssel","isofrlem","51",533
"r19.22dv","isofrlem","67",534
"f1fveq","isowe","3",535
"eqeq1","isowe","29",536
"f1fveq","f1oiso","3",537
"eqcom","f1oiso","4",538
"breq1","f1oiso","14",539
"ceqsrexv","f1oiso","17",540
"f1fveq","f1oiso","20",541
"eqcom","f1oiso","21",542
"breq2","f1oiso","26",543
"ceqsrexv","f1oiso","27",544
"fveq2","f1owe","2",545
"fveq2","f1owe","4",546
"brabg","f1owe","6",547
"funfvima2","f1oweALT","18",548
"n0","f1oweALT","22",549
"fvres","f1oweALT","45",550
"fvres","f1oweALT","46",551
"fveq2","f1oweALT","50",552
"fveq2","f1oweALT","52",553
"brab","f1oweALT","54",554
"biraldva","f1oweALT","57",555
"birexa","f1oweALT","58",556
"fveq2","f1oweALT","79",557
"fveq2","f1oweALT","81",558
"brab","f1oweALT","83",559
"f1fveq","f1oweALT","85",560
"fveq2","f1oweALT","89",561
"fveq2","f1oweALT","91",562
"brab","f1oweALT","93",563
"eqeq2","f1oweALT","104",564
"fveq2","canth","5",565
"eleq12d","canth","6",566
"elrab","canth","8",567
"sseq1","tfrlem1","8",568
"raleq","tfrlem1","10",569
"raleq","tfrlem1","12",570
"onelsst","tfrlem1","14",571
"ssel","tfrlem1","19",572
"ra4","tfrlem1","20",573
"r19.21ad","tfrlem1","22",574
"r19.21adv","tfrlem1","26",575
"onelsst","tfrlem1","27",576
"r19.20dva","tfrlem1","41",577
"raleq","tfrlem1","46",578
"fveq2","tfrlem1","47",579
"fveq2","tfrlem1","48",580
"fveq2","tfrlem2","9",581
"fveq2","tfrlem2","10",582
"rcla4v","tfrlem2","12",583
"eqeq12","tfrlem2","32",584
"fneq1","tfrlem3","3",585
"fveq1","tfrlem3","4",586
"reseq1","tfrlem3","5",587
"elab","tfrlem3","11",588
"fneq2","tfrlem3","12",589
"raleq","tfrlem3","13",590
"r19.26m","tfrlem5","20",591
"elin","tfrlem5","23",592
"fnop","tfrlem8","16",593
"ontr1","tfrlem8","43",594
"ssel","tfrlem8","44",595
"onelon","tfrlem8","60",596
"fnop","tfrlem8","63",597
"fnop","tfrlem9","12",598
"ra4","tfrlem9","19",599
"eleq2d","tfrlem9","22",600
"fveq2","tfr2","3",601
"reseq2","tfr2","4",602
"vtoclga","tfr2","qed",603
"fveq2","tfr3","11",604
"fveq2","tfr3","12",605
"hbeq","hbrdg","15",606
"hbral","hbrdg","20",607
"fveq2","rdglem1","3",608
"reseq2","rdglem1","4",609
"opeq1","rdglem2","1",610
"eqeq1","rdglem2","3",611
"eqeq1","rdglem2","5",612
"dmeq","rdglem2","6",613
"dmeq","rdglem2","11",614
"fveq1","rdglem2","15",615
"dmeq","rdglem2","20",616
"rneq","rdglem2","23",617
"ordtri3","tz7.48lem","17",618
"r2al","tz7.48lem","38",619
"eleq1","tz7.48lem","41",620
"fveq2","tz7.48lem","42",621
"eleq2","tz7.48lem","48",622
"fveq2","tz7.48lem","49",623
"eleq1","tz7.48lem","55",624
"fveq2","tz7.48lem","56",625
"eleq2","tz7.48lem","62",626
"fveq2","tz7.48lem","63",627
"onelon","tz7.48-2","2",628
"elin","tz7.48-2","6",629
"fvres","tz7.48-2","15",630
"r19.21aiv","tz7.48-2","34",631
"imaeq2","tz7.49","9",632
"ra4","tz7.49","21",633
"onelon","tz7.49","23",634
"imaeq2","tz7.49","24",635
"fveq2","tz7.49","28",636
"imaeq2","tz7.49","29",637
"rcla4v","tz7.49","33",638
"r19.23ad","tz7.49","47",639
"ssel","tz7.49","65",640
"funfvima2","tz7.49","72",641
"ra4","tz7.49","76",642
"ssel","tz7.49","79",643
"imaeq2","tz7.49","80",644
"fveq2","tz7.49","84",645
"imaeq2","tz7.49","85",646
"rcla4v","tz7.49","89",647
"r2al","tz7.49","105",648
"fveq2","abianfplem","5",649
"hbrdg","abianfplem","20",650
"hbfv","abianfplem","26",651
"rdgsucopab","abianfplem","29",652
"iuneq2i","abianfplem","42",653
"fveq2","abianfp","76",654
"eqeq12d","abianfp","78",655
"eqid","bioprabi","2",656
"opeq12","cbvoprab12","18",657
"eqcoms","oprabval4g","4",658
"eqcoms","oprabval4g","7",659
"eleq1","oprabval4g","22",660
"eleq1","oprabval4g","23",661
"eqcoms","oprabval4g","27",662
"eqcoms","oprabval4g","30",663
"oprabval2g","oprabval4g","36",664
"opeq1","elrnoprab","20",665
"opeq2","elrnoprab","35",666
"eqeq2","caoprcan","13",667
"eleq1","caoprmo","8",668
"opreq2","caoprmo","9",669
"opreq1","caoprmo","14",670
"eqeq12d","caoprmo","16",671
"vtoclga","caoprmo","17",672
"opreq1","caoprmo","30",673
"eqeq12d","caoprmo","32",674
"vtoclga","caoprmo","33",675
"eqtr3d","caoprmo","41",676
"eqid","1st2val","6",677
"oprabval2","1st2val","13",678
"fnoprab2","df1st2","7",679
"opreq2","oacl","3",680
"opreq2","omcl","3",681
"opreq2","oecl","21",682
"opreq2","oa0r","4",683
"eqeq12d","oa0r","6",684
"opreq2","om0r","3",685
"opreq2","om1r","4",686
"eqeq12d","om1r","6",687
"opreq2","oe1m","3",688
"opreq2","oaordi","10",689
"opreq2","oawordri","4",690
"opreq2","oawordri","5",691
"opreq2","oawordeulem","49",692
"onnminsb","oawordeulem","51",693
"opreq2","oawordeulem","88",694
"onnminsb","oawordeulem","90",695
"oacan","oawordeulem","154",696
"opreq2","oawordeulem","160",697
"opreq2","oaass","5",698
"opreq2","oaass","6",699
"oaord","oaass","91",700
"r19.22dv2","oaass","103",701
"onelon","oaass","117",702
"birexdva","oaass","128",703
"oaordi","oaass","140",704
"r19.23adv","oaass","147",705
"opreq2","oarec","6",706
"rexeq","oarec","7",707
"elsuc","oarec","37",708
"df-rex","oarec","45",709
"opreq2","oarec","47",710
"ceqsexv","oarec","49",711
"ordtr1","oarec","75",712
"r19.22dv2","oarec","81",713
"r19.23adv","oarec","83",714
"hbrex","oarec","87",715
"limsuc","oarec","88",716
"sucidg","oarec","90",717
"eleq2","oarec","94",718
"ra4e","oarec","97",719
"r19.23ad","oarec","103",720
"eleq2","omordi","7",721
"opreq2","omordi","8",722
"opreq2","omwordri","4",723
"opreq2","omwordri","5",724
"opreq2","odi","6",725
"opreq2","odi","8",726
"oaord","odi","96",727
"omordi","odi","150",728
"opreq2","odi","158",729
"opreq2","odi","160",730
"rcla4v","odi","163",731
"oaordi","odi","197",732
"ordelon","odi","213",733
"opreq2","odi","219",734
"opreq2","odi","221",735
"rcla4v","odi","224",736
"ordelon","odi","234",737
"r19.23adv","odi","249",738
"opreq2","omass","5",739
"opreq2","omass","6",740
"omordi","omass","56",741
"r19.21aiv","omass","69",742
"onelon","omass","92",743
"r19.22dv","omass","103",744
"opreq2","oen0","3",745
"opreq2","oeordi","4",746
"opreq2","oewordri","4",747
"opreq2","oewordri","5",748
"opreq2","oeworde","5",749
"sseq12d","oeworde","6",750
"opreq2","oelim2","85",751
"opreq2","nnacl","4",752
"opreq2","nnmcl","4",753
"opreq1","nnacom","5",754
"opreq2","nnacom","6",755
"opreq2","nnacom","26",756
"opreq2","nnacom","27",757
"opreq2","nnmsucr","7",758
"opreq2","nnmsucr","8",759
"opreq12d","nnmsucr","10",760
"opreq1","nnmcom","5",761
"opreq2","nnmcom","6",762
"opreq2","oaabs","11",763
"eqeq12d","oaabs","13",764
"ordelon","oaabs","47",765
"eldif","oaabs","57",766
"biraldv2","oaabs","62",767
"eleq2","omsmolem","1",768
"eleq2","omsmolem","5",769
"fveq2","omsmolem","6",770
"eleq2","omsmolem","9",771
"fveq2","omsmolem","16",772
"suceq","omsmolem","17",773
"rcla4v","omsmolem","20",774
"fveq2","omsmolem","38",775
"fveq2","omsmolem","40",776
"suceq","omsmolem","41",777
"rcla4v","omsmolem","44",778
"elsuc","omsmolem","52",779
"ordtri3","omsmo","31",780
"ideq","ider","4",781
"ideq","ider","7",782
"eqtrt","ider","9",783
"ideq","ider","12",784
"ideq","ider","15",785
"ideq","ider","19",786
"eleq1","ecelqsi","6",787
"eceq2","ecelqsi","7",788
"eqeq2i","qsid","5",789
"eqcom","qsid","6",790
"risset","qsid","9",791
"eqeq12","th3qlem1","35",792
"eqeq1","th3qlem1","76",793
"eceq2","th3qlem1","79",794
"eceq2","th3qlem1","81",795
"opreq12","th3qlem1","84",796
"opbrop","oprec","17",797
"opbrop","oprec","18",798
"oprabval3","oprec","20",799
"oprabval3","oprec","21",800
"hbfv","dom2d","16",801
"eleq1","dom2d","20",802
"eleq1","dom2d","23",803
"fveq2","dom2d","28",804
"ideq","idssen","4",805
"f1oeq3","idssen","6",806
"eqeq1","2dom","6",807
"eqeq1","fundmen","18",808
"opeq1","fundmen","25",809
"eqeq1","fundmen","34",810
"opeq1","fundmen","41",811
"eqeq2d","mapsnen","19",812
"eleq1","mapsnen","30",813
"opeq2","mapsnen","31",814
"ceqsexv","mapsnen","35",815
"f1fveq","xpdom2","65",816
"opth","xpdom2","71",817
"eqeq12","xpdom2","79",818
"opth","xpdom2","83",819
"elin","pw2en","41",820
"eleq1","pw2en","44",821
"eleq1","pw2en","45",822
"opelopab","pw2en","52",823
"eleq2","pw2en","112",824
"eleq2","pw2en","143",825
"cleqfvf","pw2en","193",826
"sseq1","sbth","12",827
"imaeq2","sbth","13",828
"difeq2","sbth","18",829
"sneqr","canth2","7",830
"sneq","canth2","8",831
"coeq2","mapenlem1","7",832
"fvopab4","mapenlem1","15",833
"cleqfv","mapenlem2","51",834
"unineq","mapdom2","42",835
"breq1","ssenen","27",836
"elab","ssenen","28",837
"breq1","ssenen","65",838
"elab","ssenen","66",839
"suc11","limenpsi","14",840
"eqeq1","nneneq","6",841
"breq1","nneneq","9",842
"eqeq1","nneneq","10",843
"eqeq1","nneneq","14",844
"eqeq1","nneneq","18",845
"suceq","nneneq","51",846
"breq2","nneneq","64",847
"eqeq2","nneneq","65",848
"breq2","php3","94",849
"breq2","ominf","1",850
"psseq2","pssnn","13",851
"rexeq","pssnn","14",852
"eleq1","pssnn","30",853
"sseld","pssnn","35",854
"elsuci","pssnn","36",855
"ssrdv","pssnn","45",856
"dfpss2","pssnn","47",857
"elelsuc","pssnn","49",858
"r19.22i2","pssnn","51",859
"eleq2","pssnn","65",860
"eldifi","pssnn","66",861
"elsuci","pssnn","69",862
"eleq1a","pssnn","71",863
"pssnel","pssnn","80",864
"psseq1","pssnn","87",865
"breq1","pssnn","88",866
"ordsucelsuc","pssnn","103",867
"snssi","pssnn","108",868
"elnn","pssnn","133",869
"df-rex","pssnn","143",870
"breq2","pssnn","144",871
"eqelsuc","pssnn","152",872
"breq2","pssnn","156",873
"rcla4ev","pssnn","157",874
"breq2","ssfi","37",875
"eleq1","unblem1","27",876
"fveq2","unblem2","5",877
"eleq1","unblem2","14",878
"hbfv","unblem2","36",879
"frsucopab","unblem2","43",880
"hbfv","unblem3","23",881
"frsucopab","unblem3","30",882
"sucssel","unbnn2","7",883
"ordtri1","isfinite2","16",884
"ssel2","isfinite2","17",885
"biraldva","isfinite2","23",886
"opreq2","unfilem2","13",887
"fvopab4","unfilem2","15",888
"opreq2","unfilem2","16",889
"fvopab4","unfilem2","18",890
"nnacan","unfilem2","20",891
"breq2","unfi","27",892
"breq2","unfi","34",893
"ineq1","fiint","1",894
"ineq2","fiint","5",895
"breq1","fiint","13",896
"eleq2","zfregcl","2",897
"eleq2","zfregcl","4",898
"df-ral","zfregcl","11",899
"df-rex","zfregcl","13",900
"eleq1","eirrv","1",901
"elsn","eirrv","11",902
"eleq1","eirrv","15",903
"rcla4v","eirrv","17",904
"eleq2","eirr","1",905
"eleq1","en2lp","1",906
"eleq2","en2lp","2",907
"hbrdg","inf0","22",908
"hbfv","inf0","26",909
"frsucopab","inf0","30",910
"eleq2","inf0","43",911
"eleq2","inf0","60",912
"eleq2","inf0","61",913
"eleq2","inf0","62",914
"eleq1","inf0","70",915
"eleq1","inf0","71",916
"n0i","inf1","2",917
"dfss2","inf2","3",918
"eluni","inf2","4",919
"sseq2","inf3lema","6",920
"ineq1","inf3lema","8",921
"eqeqan12rd","inf3lema","12",922
"inf3lema","inf3lemd","13",923
"ssrdv","inf3lemd","16",924
"fveq2","inf3lem1","9",925
"suceq","inf3lem1","10",926
"inf3lema","inf3lem1","30",927
"inf3lema","inf3lem1","41",928
"fveq2","inf3lem2","9",929
"ssel","inf3lem2","28",930
"eluni","inf3lem2","29",931
"inf3lema","inf3lem2","36",932
"elin","inf3lem2","39",933
"eleq2","inf3lem2","42",934
"pssnel","inf3lem2","58",935
"eldifi","inf3lem3","13",936
"inf3lema","inf3lem3","19",937
"fveq2","inf3lem5","14",938
"inf3lem5","inf3lem6","7",939
"inf3lem5","inf3lem6","16",940
"ordtri3","inf3lem6","28",941
"eleq2","inf4","8",942
"df-rex","inf4","16",943
"sucel","inf4","18",944
"df-rex","inf4","19",945
"df-rex","zfinf","3",946
"sucel","zfinf","5",947
"df-rex","zfinf","6",948
"df-ral","zfinf","9",949
"peano5","omex","2",950
"r19.20i2","omex","4",951
"suceq","dfom3","5",952
"rcla4v","dfom3","7",953
"elintab","dfom3","13",954
"elintab","dfom3","26",955
"eleq2","dfom3","32",956
"elom3","dfom4","1",957
"suceq","infensuc","6",958
"breq12d","infensuc","7",959
"ordeirr","infensuc","27",960
"disjsn","infensuc","29",961
"hbfv","trcl","40",962
"hbfv","trcl","51",963
"frsucopab","trcl","57",964
"elunii","trcl","62",965
"fveq2","trcl","73",966
"fveq2","trcl","87",967
"hbfv","trcl","122",968
"hbfv","trcl","133",969
"frsucopab","trcl","139",970
"fveq2","trcl","149",971
"trel","zfregs","4",972
"elin","zfregs","10",973
"sseli","zfregs","20",974
"elin","zfregs","32",975
"sseq1","setind","1",976
"eleq1","setind","2",977
"fveq2","r1tr","4",978
"ssel","r1tr","24",979
"ssrdv","r1tr","33",980
"ra4","r1tr","48",981
"r19.22d","r1tr","51",982
"eleq2","r1ord","5",983
"fveq2","r1ord","6",984
"eleq1","tz9.12lem1","8",985
"eqeq1","tz9.12lem1","12",986
"opelopab","tz9.12lem1","13",987
"fveq2","tz9.12lem3","3",988
"rcla4ev","tz9.12lem3","5",989
"eleq1","tz9.12lem3","11",990
"eqeq1","tz9.12lem3","15",991
"opelopab","tz9.12lem3","16",992
"fveq2","tz9.12lem3","43",993
"rcla4ev","tz9.12lem3","45",994
"eleq1","tz9.12lem3","50",995
"fvopabg","tz9.12lem3","53",996
"hbfv","tz9.12lem3","71",997
"hbfv","tz9.12lem3","84",998
"hbel","tz9.12lem3","86",999
"ssel","tz9.13","3",1000
"eleq1","tz9.13","5",1001
"elab","tz9.13","7",1002
"r19.21aiv","tz9.13","9",1003
"eleq1","tz9.13","14",1004
"elab","tz9.13","16",1005
"suceq","rankr1","33",1006
"onintss","rankr1","36",1007
"suceq","rankr1","61",1008
"onintss","rankr1","64",1009
"fveq2","r1pwcl","25",1010
"eluni2","rankuni","12",1011
"rankel","rankuni","19",1012
"elintrab","rankun","7",1013
"eleq2","rankun","24",1014
"fveq2","rankonid","1",1015
"eqeq12d","rankonid","3",1016
"eleq1","rankonid","7",1017
"dfss3","rankonid","11",1018
"fveq2","scottex","19",1019
"elrab","scottex","21",1020
"fveq2","scott0","51",1021
"rcla4ev","scott0","53",1022
"fveq2","scottexs","7",1023
"fveq2","scott0s","9",1024
"elin","cp","4",1025
"hbin","cp","12",1026
"df-rex","cp","14",1027
"elin","bnd2","18",1028
"birex2","bnd2","22",1029
"breq1","kardex","4",1030
"elab","kardex","5",1031
"breq1","kardex","8",1032
"elab","kardex","9",1033
"breq1","karden","20",1034
"fveq2","karden","21",1035
"breq1","karden","26",1036
"fveq2","karden","27",1037
"breq1","karden","43",1038
"elab","karden","44",1039
"breq1","karden","47",1040
"elab","karden","48",1041
"eleq1","aceq1","3",1042
"eleq1","aceq1","12",1043
"reueqd","aceq1","15",1044
"raleqd","aceq1","16",1045
"eleq1","aceq1","18",1046
"reueqd","aceq1","21",1047
"raleqd","aceq1","22",1048
"df-reu","aceq1","32",1049
"df-rex","aceq1","38",1050
"eleq1","aceq1","39",1051
"eleq2","aceq1","40",1052
"eleq2","aceq1","41",1053
"df-ral","aceq1","54",1054
"eleq1","aceq1","60",1055
"df-ral","aceq1","68",1056
"df-ral","aceq2","3",1057
"n0","aceq2","6",1058
"eleq2","aceq2","7",1059
"eleq2","aceq2","8",1060
"eleq1","aceq2","12",1061
"eleq1","aceq3lem","17",1062
"breq1","aceq3lem","18",1063
"eqeq1","aceq3lem","23",1064
"opelopab","aceq3lem","25",1065
"breq1","aceq3lem","52",1066
"fvopab4","aceq3lem","56",1067
"breq2","aceq3lem","60",1068
"sseq1","aceq3lem","98",1069
"fneq1","aceq3lem","99",1070
"sseq2","aceq3","1",1071
"dmeq","aceq3","2",1072
"elunii","aceq3","13",1073
"df-xp","aceq3","17",1074
"eleq1","aceq3","33",1075
"eleq2","aceq3","34",1076
"elab","aceq3","37",1077
"n0","aceq3","38",1078
"biabrdv","aceq3","52",1079
"eleq1","aceq3","58",1080
"eleq2","aceq3","59",1081
"eleq1","aceq3","61",1082
"brab","aceq3","64",1083
"r19.21aiv","aceq3","72",1084
"fveq1","aceq4","2",1085
"fveq2","aceq4","7",1086
"fvopab4","aceq4","10",1087
"birala","aceq4","13",1088
"fnopab2","aceq4","17",1089
"funopabex2","aceq4","20",1090
"elin","aceq5lem1","1",1091
"elxp","aceq5lem1","2",1092
"eleq1","aceq5lem1","8",1093
"elsn","aceq5lem1","10",1094
"opeq1","aceq5lem1","22",1095
"opeq1","aceq5lem1","24",1096
"ceqsexv","aceq5lem1","28",1097
"df-rex","aceq5lem2","10",1098
"opelxp","aceq5lem2","27",1099
"elsn","aceq5lem2","28",1100
"eqcom","aceq5lem2","29",1101
"eleq1","aceq5lem2","38",1102
"eleq2","aceq5lem2","39",1103
"ceqsexv","aceq5lem2","41",1104
"3eqtr3g","aceq5lem3","33",1105
"sneq","aceq5lem3","34",1106
"xpeq2","aceq5lem3","37",1107
"eqcom","aceq5lem3","40",1108
"eleq1","aceq5lem3","47",1109
"ceqsexv","aceq5lem3","48",1110
"df-rex","aceq5lem3","50",1111
"eqeq1","aceq5lem4","6",1112
"eqeq1","aceq5lem4","8",1113
"elab","aceq5lem4","11",1114
"eleq2","aceq5lem4","15",1115
"elxp","aceq5lem4","16",1116
"eleq2","aceq5lem4","20",1117
"elxp","aceq5lem4","21",1118
"opeq1","aceq5lem4","28",1119
"elsn","aceq5lem4","31",1120
"opeq1","aceq5lem4","35",1121
"elsn","aceq5lem4","38",1122
"opth","aceq5lem4","47",1123
"sneq","aceq5lem4","52",1124
"xpeq2","aceq5lem4","55",1125
"eqeq12","aceq5lem4","58",1126
"r19.23aiv","aceq5lem4","62",1127
"r19.23adv","aceq5lem4","64",1128
"eqeq1","aceq5lem4","67",1129
"eqeq1","aceq5lem4","69",1130
"elab2","aceq5lem4","72",1131
"eqeq1","aceq5lem4","75",1132
"eqeq1","aceq5lem4","77",1133
"elab2","aceq5lem4","80",1134
"sneq","aceq5lem4","82",1135
"xpeq2","aceq5lem4","85",1136
"disj1","aceq5lem4","95",1137
"eleq1d","aceq5lem5","42",1138
"r19.21aiv","aceq5lem5","51",1139
"fveq2","aceq5","2",1140
"eleq12d","aceq5","4",1141
"eqeq2","aceq5","5",1142
"ineq2","aceq5","7",1143
"rcla4v","aceq5","11",1144
"eleq1","aceq5","12",1145
"disj","aceq5","15",1146
"eleq1","aceq5","22",1147
"fveq2","aceq5","28",1148
"r19.23adv","aceq5","35",1149
"elin","aceq5","42",1150
"fveq2","aceq5","49",1151
"eleq12d","aceq5","51",1152
"rcla4v","aceq5","52",1153
"fnfvrn","aceq5","53",1154
"eqeq2","aceq5","68",1155
"r19.20dva","aceq5","75",1156
"eqeq1","aceq5","77",1157
"raleq","aceq5","108",1158
"eleq2","aceq6a","1",1159
"eleq1","aceq6a","2",1160
"df-rab","aceq6a","7",1161
"df-rab","aceq6a","8",1162
"fvopab4","aceq6a","15",1163
"r19.20i","aceq6a","20",1164
"funopabex2","aceq6a","22",1165
"ra4","aceq6b","3",1166
"eleq1","aceq6b","5",1167
"eleq1","aceq6b","6",1168
"eqid","aceq6b","11",1169
"eqeq1","aceq6b","12",1170
"eqeq1","aceq6b","14",1171
"rcla4ev","aceq6b","16",1172
"fveq2","aceq6b","18",1173
"preq2","aceq6b","21",1174
"eleq2","aceq6b","38",1175
"eqeq1","aceq6b","49",1176
"elab","aceq6b","52",1177
"eqeq1","aceq6b","53",1178
"fveq2","aceq6b","55",1179
"eleq2","aceq6b","57",1180
"rcla4v","aceq6b","60",1181
"prel12","aceq6b","66",1182
"eleq2","aceq6b","67",1183
"eleq2","aceq6b","68",1184
"eleq2","aceq6b","74",1185
"preleq","aceq6b","85",1186
"fveq2","aceq6b","87",1187
"r19.23aiv","aceq6b","98",1188
"df-reu","aceq6b","112",1189
"r19.21ai","aceq6b","117",1190
"hbco","ac6lem","135",1191
"eqeq1","ac6","5",1192
"sseli","kmlem1","13",1193
"sseli","kmlem1","15",1194
"r19.20i2","kmlem1","17",1195
"r19.20i2","kmlem1","19",1196
"eqeq1","kmlem1","20",1197
"elrab","kmlem1","22",1198
"eqeq1","kmlem1","26",1199
"elrab","kmlem1","28",1200
"r19.20i2","kmlem1","32",1201
"raleq","kmlem1","37",1202
"raleqd","kmlem1","38",1203
"raleq","kmlem1","39",1204
"ineq2","kmlem2","1",1205
"eleq2","kmlem2","9",1206
"elssuni","kmlem2","17",1207
"sseld","kmlem2","18",1208
"disjsn","kmlem2","20",1209
"biraldva","kmlem2","31",1210
"elun","kmlem2","36",1211
"eleq1","kmlem2","47",1212
"dfnul3","kmlem3","2",1213
"df-rex","kmlem3","9",1214
"eldif","kmlem3","10",1215
"elsn","kmlem3","11",1216
"eqcom","kmlem3","12",1217
"elin","kmlem3","25",1218
"eluni","kmlem3","34",1219
"birabi","kmlem3","41",1220
"eleq1","kmlem4","2",1221
"eqeq2","kmlem4","3",1222
"eleq2","kmlem4","6",1223
"cla4v","kmlem4","9",1224
"eldif","kmlem4","11",1225
"eluni","kmlem4","13",1226
"eldif","kmlem4","17",1227
"elsn","kmlem4","18",1228
"eqcom","kmlem4","19",1229
"disj","kmlem4","43",1230
"df-rex","kmlem6","3",1231
"n0","kmlem6","5",1232
"eqeq12","kmlem8","8",1233
"difeq1","kmlem8","9",1234
"sneq","kmlem8","10",1235
"r19.23aivv","kmlem8","20",1236
"eqeq1","kmlem8","23",1237
"elab2","kmlem8","25",1238
"eqeq1","kmlem8","27",1239
"elab2","kmlem8","29",1240
"difeq1","kmlem8","30",1241
"sneq","kmlem8","31",1242
"snssi","kmlem10","2",1243
"elsn","kmlem10","14",1244
"difeq1","kmlem10","26",1245
"sneq","kmlem10","27",1246
"iunxsn","kmlem10","33",1247
"difeq1","kmlem11","2",1248
"sneq","kmlem11","3",1249
"difeq1","kmlem11","11",1250
"sneq","kmlem11","12",1251
"r19.20i","kmlem11","32",1252
"eqeq1","kmlem11","40",1253
"elab","kmlem11","42",1254
"raleq","kmlem12","4",1255
"raleqd","kmlem12","5",1256
"raleq","kmlem12","6",1257
"ineq2","kmlem12","11",1258
"df-rex","kmlem13","2",1259
"n0","kmlem13","7",1260
"eqeq1","kmlem14","4",1261
"ineq1","kmlem14","6",1262
"raleqd","kmlem14","10",1263
"df-rex","kmlem14","12",1264
"eleq1","kmlem14","13",1265
"df-ral","kmlem14","17",1266
"eqeq2","kmlem14","21",1267
"ineq2","kmlem14","23",1268
"df-rex","kmlem14","27",1269
"elin","kmlem14","34",1270
"elin","kmlem15","6",1271
"eleq1","kmlem15","8",1272
"elin","kmlem15","10",1273
"eqcom","kmlem15","12",1274
"df-ral","kmlem15","21",1275
"rneq","numth","5",1276
"eqeqan12rd","numth","9",1277
"funfvima2","zornlem2","13",1278
"r2al","zornlem4","43",1279
"onelon","zornlem5","19",1280
"df-ral","zornlem5","27",1281
"r19.23ad","zornlem5","30",1282
"onelon","zornlem6","12",1283
"onelon","zornlem6","13",1284
"eqeq12","zornlem6","26",1285
"fveq2","zornlem6","27",1286
"ordtri3or","zornlem6","41",1287
"imaeq2","zornlem6","57",1288
"rcla4v","zornlem6","63",1289
"imaeq2","zornlem6","65",1290
"rcla4v","zornlem6","71",1291
"df-rex","zornlem6","82",1292
"df-rex","zornlem6","86",1293
"imaeq2","zornlem7","10",1294
"breq1","zornlem7","44",1295
"breq2","zornlem7","61",1296
"elrab","zornlem7","63",1297
"breq1","zornlem7","68",1298
"psseq1","zorn2lem","3",1299
"psseq2","zorn2lem","4",1300
"brab","zorn2lem","qed",1301
"breq2","zorn","4",1302
"breq1","zorn","6",1303
"rneq","zorn","12",1304
"rneq","zorn","17",1305
"breq1","zorn","22",1306
"eleq1","zorn","29",1307
"breq2","zorn","30",1308
"eqeqan12rd","zorn","40",1309
"sspsstri","zorn2","8",1310
"sspss","zorn2","19",1311
"breq2","hta","36",1312
"breq1","hta","47",1313
"hbel","hta","70",1314
"hbel","hta","79",1315
"breq2","hta","82",1316
"eqeq1","unxpdomlem","3",1317
"ifeq2","unxpdomlem","5",1318
"eqeq1","unxpdomlem","10",1319
"ifeq2","unxpdomlem","12",1320
"eqeq1","unxpdomlem","14",1321
"rcla42ev","unxpdomlem","18",1322
"eqid","unxpdomlem","20",1323
"eqtr4d","unxpdomlem","25",1324
"eqeq1","unxpdomlem","30",1325
"ifeq2","unxpdomlem","32",1326
"eqeq1","unxpdomlem","37",1327
"ifeq2","unxpdomlem","39",1328
"eqeq1","unxpdomlem","41",1329
"rcla42ev","unxpdomlem","45",1330
"eqeq1","unxpdomlem","56",1331
"ifeq2","unxpdomlem","58",1332
"eqeq1","unxpdomlem","63",1333
"ifeq2","unxpdomlem","65",1334
"eqeq1","unxpdomlem","67",1335
"rcla42ev","unxpdomlem","71",1336
"eqtrd","unxpdomlem","75",1337
"eqeq1","unxpdomlem","82",1338
"ifeq2","unxpdomlem","84",1339
"eqeq1","unxpdomlem","89",1340
"ifeq2","unxpdomlem","91",1341
"eqeq1","unxpdomlem","93",1342
"rcla42ev","unxpdomlem","97",1343
"eqid","unxpdomlem","99",1344
"breq1","iscard2","15",1345
"elrab","iscard2","16",1346
"onelon","ondomon","4",1347
"onelsst","ondomon","5",1348
"breq1","ondomon","16",1349
"elrab","ondomon","17",1350
"breq1","ondomon","18",1351
"elrab","ondomon","19",1352
"breq1","ondomcard","4",1353
"elrab","ondomcard","5",1354
"fveq2","carduni","2",1355
"eqeq12d","carduni","4",1356
"rcla4v","carduni","5",1357
"fveq2","carduni","18",1358
"eqeq12d","carduni","20",1359
"rcla4v","carduni","21",1360
"fveq2","carduni","50",1361
"eqeq12d","carduni","52",1362
"rcla4v","carduni","53",1363
"eqeq1","cardiun","3",1364
"elab","cardiun","5",1365
"breq2","cardmin","10",1366
"elrab","cardmin","11",1367
"fveq2","alephon","3",1368
"rdgsucopab","alephon","19",1369
"rdgsucopabn","alephon","33",1370
"fveq2","alephcard","5",1371
"fveq2","alephcard","7",1372
"eleq2","alephordi","5",1373
"fveq2","alephordi","6",1374
"fveq2","alephle","2",1375
"sseq12d","alephle","3",1376
"alephord2i","alephle","7",1377
"onelon","alephle","9",1378
"r19.20dva","alephle","15",1379
"fveq2","cardaleph","47",1380
"onnminsb","cardaleph","49",1381
"fveq2","cardaleph","97",1382
"onnminsb","cardaleph","99",1383
"aleph11","alephiso","12",1384
"alephord2","alephiso","23",1385
"hbfv","alephfplem2","16",1386
"frsucopab","alephfplem2","19",1387
"fveq2","alephfplem3","5",1388
"eluni","alephfp","10",1389
"eleq2","alephfp","28",1390
"fveq2","alephval2","26",1391
"rcla4v","alephval2","28",1392
"breq2","alephval2","92",1393
"elrab","alephval2","94",1394
"fveq2","alephval3","59",1395
"eqeq12d","alephval3","61",1396
"sseq2","alephval3","62",1397
"eqeq1","alephval3","63",1398
"elab","alephval3","67",1399
"sseq2","cflem","3",1400
"rcla4ev","cflem","4",1401
"ssel","cfub","2",1402
"onelsst","cfub","6",1403
"eluni","cfub","11",1404
"df-rex","cfub","12",1405
"sucssel","cflim","7",1406
"eluni2","cflim","10",1407
"eqeq1","cardcf","10",1408
"elab","cardcf","13",1409
"eqeq1","cardcf","33",1410
"elab","cardcf","36",1411
"sseq2","cflecard","4",1412
"rcla4ev","cflecard","5",1413
"eqeq1","cfeq0","5",1414
"elab","cfeq0","8",1415
"en2lp","axunndlem1","2",1416
"eleq2","axpowndlem3","19",1417
"n0","axpowndlem3","28",1418
"en2lp","axacndlem5","164",1419
"vtoclf","zfcndrep","31",1420
"eleq1","ltpiord","2",1421
"ordtri2","ltsopi","1",1422
"ltpiord","ltsopi","5",1423
"ltpiord","ltsopi","6",1424
"ontr1","ltsopi","14",1425
"ltpiord","ltsopi","16",1426
"ltpiord","ltsopi","18",1427
"ltpiord","ltsopi","21",1428
"eleq1","indpi","28",1429
"breq2","indpi","29",1430
"eqvinc","indpi","113",1431
"gencl","indpi","115",1432
"mulcanpi","enqer","10",1433
"opreq12","addpipq","8",1434
"opreq12","addpipq","9",1435
"opreq12","addpipq","12",1436
"opreq12","addpipq","13",1437
"opreq12","addpipq","18",1438
"opreq12","addpipq","19",1439
"opreq12","addpipq","22",1440
"opreq12","addpipq","27",1441
"opreq12","addpipq","28",1442
"opreq12","addpipq","31",1443
"opreq12","mulpipq","8",1444
"opreq12","mulpipq","9",1445
"opreq12","mulpipq","12",1446
"opreq12","mulpipq","13",1447
"opreq12","mulpipq","18",1448
"opreq12","mulpipq","19",1449
"opreq12","mulpipq","23",1450
"opreq12","mulpipq","24",1451
"eqeq2","ltsopq","14",1452
"eleq2","elnp","10",1453
"rexeq","genpv","14",1454
"rexeq","genpv","16",1455
"oprabval2","genpv","19",1456
"eqeq1","genpv","21",1457
"eleq1","genpv","25",1458
"eleq1","genpv","26",1459
"opreq12","genpv","28",1460
"sotrieq","distrlem4pr","73",1461
"opreq1","distrlem4pr","78",1462
"psslinpr","ltsopr","15",1463
"opeq1","prlem934a","9",1464
"eleq1","prlem934a","30",1465
"opreq1","prlem934a","31",1466
"opreq2","ltexprlem3","21",1467
"elab2","ltexprlem3","25",1468
"opreq2","ltexprlem4","68",1469
"elab2","ltexprlem4","72",1470
"opreq2","ltexpri","8",1471
"opreq2","ltexpri","15",1472
"opreq2","ltexpri","21",1473
"eleq1","prlem936","84",1474
"opreq1","prlem936","85",1475
"cla4ev","prlem936","89",1476
"breq1","reclem2pr","66",1477
"elab2","reclem2pr","69",1478
"breq1","reclem2pr","87",1479
"elab2","reclem2pr","90",1480
"breq1","recexpr","4",1481
"breq1","recexpr","9",1482
"n0","suplem1pr","3",1483
"eluni","suplem1pr","14",1484
"prcdpq","suplem1pr","45",1485
"elunii","suplem1pr","51",1486
"eluni","suplem1pr","56",1487
"prnmax","suplem1pr","62",1488
"elunii","suplem1pr","69",1489
"eluni","suplem1pr","78",1490
"sotric","suplem2pr","10",1491
"sspss","suplem2pr","16",1492
"eqcom","suplem2pr","17",1493
"addcanpr","enrer","11",1494
"opreq12","addsrpr","8",1495
"opreq12","addsrpr","9",1496
"opreq12","addsrpr","12",1497
"opreq12","addsrpr","13",1498
"opreq12","addsrpr","18",1499
"opreq12","addsrpr","19",1500
"opreq12","addsrpr","23",1501
"opreq12","addsrpr","24",1502
"opreq12","mulsrpr","8",1503
"opreq12","mulsrpr","9",1504
"opreq12","mulsrpr","12",1505
"opreq12","mulsrpr","13",1506
"opreq12","mulsrpr","18",1507
"opreq12","mulsrpr","19",1508
"opreq12","mulsrpr","22",1509
"opreq12","mulsrpr","23",1510
"opreq12","mulsrpr","28",1511
"opreq12","mulsrpr","29",1512
"opreq12","mulsrpr","32",1513
"opreq12","mulsrpr","33",1514
"eqeq2","ltsosr","14",1515
"opreq1","suppsr","19",1516
"elab2","suppsr","24",1517
"opreq1","suppsr","47",1518
"elab2","suppsr","52",1519
"opreq1","suppsr","98",1520
"elab2","suppsr","103",1521
"eleq1","suppsr2","4",1522
"breq2","suppsr2","5",1523
"eleq1","suppsr2","8",1524
"eleq1","suppsr2","9",1525
"breq1","suppsr2","10",1526
"opreq1","suppsr2","48",1527
"eleq1","suppsr2","64",1528
"breq2","suppsr2","65",1529
"eleq1","suppsr2","75",1530
"breq2","suppsr2","76",1531
"eleq1","suppsr3","3",1532
"breq2","suppsr3","4",1533
"elab2","suppsr3","6",1534
"sotric","suppsr3","45",1535
"breq2","suppsr3","53",1536
"eleq1","suppsr3","104",1537
"breq2","suppsr3","105",1538
"elab2","suppsr3","107",1539
"opreq1","supsrlem4","7",1540
"eleq1","supsrlem6","3",1541
"breq2","supsrlem6","4",1542
"opreq1","supsr","6",1543
"opeq1","supre","15",1544
"elab2","supre","17",1545
"opeq1","supre","38",1546
"elab2","supre","40",1547
"opeq1","supre","76",1548
"elab2","supre","78",1549
"eqeq2","ltsor","16",1550
"sotric","ltsor","32",1551
"eqresr","ltsor","38",1552
"opeq1","axsup","29",1553
"opreq2","negeu","3",1554
"addcant","negeu","32",1555
"opreq2","receu","4",1556
"mulcant2","receu","33",1557
"axlttri","ltso","1",1558
"eleq2","peano5nn","3",1559
"eleq1","peano2nn","3",1560
"opreq1","peano2nn","4",1561
"elintab","peano2nn","12",1562
"eleq1","nnind","23",1563
"elab","nnind","25",1564
"dfsbcq","nn1suc","6",1565
"dfsbcq","nn1suc","8",1566
"dfsbcq","nn1suc","9",1567
"opreq2","nnaddclt","4",1568
"opreq2","nnmulclt","4",1569
"breq2","nnge1t","2",1570
"eqeq2","nnleltp1t","37",1571
"opreq1","nnleltp1t","41",1572
"breq2","nnleltp1t","43",1573
"eqeq2","nnleltp1t","44",1574
"eqeq2","nnleltp1t","51",1575
"eqeq2","nnleltp1t","58",1576
"breq1","nnleltp1t","72",1577
"breq1","nnleltp1t","73",1578
"eqeq1","nnleltp1t","74",1579
"nn1suc","nnleltp1t","97",1580
"breq1","nnleltp1t","111",1581
"breq1","nnleltp1t","112",1582
"eqeq1","nnleltp1t","113",1583
"breq1","nnleltp1t","134",1584
"breq1","nnleltp1t","135",1585
"eqeq1","nnleltp1t","136",1586
"rcla4v","nnleltp1t","139",1587
"addcant","nnleltp1t","168",1588
"nn1suc","nnleltp1t","180",1589
"breq1","nnleltp1t","184",1590
"breq1","nnleltp1t","185",1591
"eqeq1","nnleltp1t","186",1592
"breq2","nnsub","7",1593
"opreq1","nnsub","8",1594
"breq1","sup2","21",1595
"eleq1","sup2","46",1596
"breq2","sup2","47",1597
"leloet","sup3","5",1598
"axlttri","arch","6",1599
"eqcom","arch","9",1600
"eleq1","uzind","60",1601
"eqeq12","uzind","78",1602
"opreq1","uzind","79",1603
"breq2","uzind3","7",1604
"elrab","uzind3","8",1605
"breq1","uzwo","4",1606
"breq1","uzwo","10",1607
"breq2","uzwo","14",1608
"elrab","uzwo","15",1609
"breq1","uzwo","22",1610
"rcla4ev","uzwo","24",1611
"letri3t","uzwo","28",1612
"eleq1a","uzwo","48",1613
"uzind3","uzwo","71",1614
"breq1","uzwo","72",1615
"rcla4ev","uzwo","74",1616
"breq2","uzwo2","7",1617
"rcla4v","uzwo2","8",1618
"breq2","uzwo2","9",1619
"rcla4v","uzwo2","10",1620
"letri3t","uzwo2","17",1621
"breq1","uzwo2","28",1622
"breq1","nnwoOLD","4",1623
"breq1","nnwoOLD","10",1624
"breq1","nnwoOLD","18",1625
"rcla4ev","nnwoOLD","20",1626
"letri3t","nnwoOLD","24",1627
"eleq1a","nnwoOLD","44",1628
"nnind","nnwoOLD","61",1629
"breq1","nnwoOLD","62",1630
"rcla4ev","nnwoOLD","64",1631
"hbel","nnwof","5",1632
"eleq1","nnwof","9",1633
"breq2","nnwof","10",1634
"hbel","nnwof","16",1635
"hbel","nnwof","18",1636
"eleq1","nnwof","24",1637
"breq1","nnwof","25",1638
"elrab","nnwos","13",1639
"dfsbcq","nn0indALT","8",1640
"vsbcint","nn0indALT","9",1641
"eqeq2","nn0indALT","25",1642
"breq2","uzwo3lem2","4",1643
"rcla4v","uzwo3lem2","5",1644
"breq1","uzwo3lem2","7",1645
"breq2","uzwo3lem2","9",1646
"breq2","uzwo3lem2","21",1647
"elrab","uzwo3lem2","22",1648
"breq2","uzwo3lem2","29",1649
"breq2","uzwo3lem2","39",1650
"breq2","uzwo3","4",1651
"breq1","uzwo3","7",1652
"breq2","zmin","3",1653
"elrab","zmin","4",1654
"breq2","zmin","5",1655
"elrab","zmin","6",1656
"breq2","uzinfm","10",1657
"elrab","uzinfm","11",1658
"breq2","uzinfm","44",1659
"elrab","uzinfm","45",1660
"breq1","flleltt","2",1661
"opreq1","flleltt","3",1662
"breq1","flval3t","24",1663
"elrab","flval3t","25",1664
"breq1","flval3t","60",1665
"elrab","flval3t","61",1666
"breq1","flval3t","81",1667
"elrab","flval3t","82",1668
"breq1","flval3t","115",1669
"elrab","flval3t","116",1670
"opreq2","qnegclt","17",1671
"rcla42ev","qnegclt","19",1672
"breq2","monoord","8",1673
"fveq2","monoord","9",1674
"fveq2","monoord","54",1675
"opreq1","monoord","55",1676
"vtoclga","monoord","58",1677
"hbfv","om2uzsuc","17",1678
"frsucopab","om2uzsuc","30",1679
"fveq2","om2uzuz","5",1680
"eleq2","om2uzlt","8",1681
"fveq2","om2uzlt","9",1682
"breq2","om2uzran","15",1683
"elrab","om2uzran","16",1684
"eleq1","om2uzran","18",1685
"eleq1","om2uzran","20",1686
"uzind","om2uzran","53",1687
"ordtri3","om2uzf1o","28",1688
"om2uzlt","om2uzf1o","33",1689
"om2uzlt","om2uzf1o","34",1690
"fveq2","seqlem1","6",1691
"eqeq12d","seqlem1","9",1692
"fveq2","seqlem1","39",1693
"dfsbcq","seqlem1","53",1694
"fveq2","seqsuclem","11",1695
"fveq2","seqsuclem","13",1696
"fveq2","seqsuclem","14",1697
"eqeq1","seqsuclem","20",1698
"fveq2","seqrn","6",1699
"fveq2","seqrn","12",1700
"nnind","seqrn","49",1701
"fveq2","serrecl","4",1702
"fveq2","sermono","13",1703
"vtoclga","sermono","15",1704
"fveq2","sermconst","9",1705
"fveq2","sermconst","10",1706
"opreq2","1expt","3",1707
"opreq2","expcllem","6",1708
"opreq2","expeq0t","5",1709
"opreq2","expgt0t","4",1710
"opreq2","expgt1t","4",1711
"opreq2","mulexpt","7",1712
"opreq2","mulexpt","8",1713
"opreq2","mulexpt","9",1714
"opreq2","recexpt","6",1715
"opreq2","recexpt","7",1716
"opreq2","expaddt","7",1717
"opreq2","expaddt","9",1718
"opreq2","bernneq","6",1719
"opreq2","bernneq","8",1720
"opreq1","nneo","101",1721
"opreq1","nneo","104",1722
"breq2","sqrval","9",1723
"elrab","sqrval","10",1724
"breq2","sqrlem24","3",1725
"opreq12","sqrlem24","4",1726
"breq2","sqrgt0i","3",1727
"opreq12","sqrgt0i","4",1728
"breq2","sqrlem26","3",1729
"opreq12","sqrlem26","4",1730
"opreq1","sqr2irrlem3","1",1731
"opreq1","sqr2irrlem3","5",1732
"breq1","sqr2irrlem3","11",1733
"opreq1","sqr2irrlem3","12",1734
"rcla4v","sqr2irrlem3","17",1735
"crut","creur","2",1736
"opreq1","creur","21",1737
"opreq1","creur","24",1738
"crut","creui","4",1739
"opreq1","creui","23",1740
"opreq1","creui","27",1741
"opreq2","absexpt","6",1742
"opreq2","absexpt","8",1743
"breq2","seqbnd","6",1744
"breq2","seqbnd","151",1745
"breq1","sequblem","28",1746
"fveq2","sequblem","29",1747
"rcla4v","sequblem","33",1748
"breq1","sequblem","54",1749
"elrab","sequblem","55",1750
"breq1","sequblem","67",1751
"elrab","sequblem","68",1752
"breq1","sequb","5",1753
"breq1","sequb","13",1754
"fveq2","cau2","4",1755
"leloet","cau2","22",1756
"breq1","cvg1","13",1757
"fveq2","caure","5",1758
"fveq2","caure","6",1759
"vtoclga","caure","9",1760
"fveq2","caure","10",1761
"fveq2","caure","11",1762
"vtoclga","caure","14",1763
"fveq2","cauim","5",1764
"fveq2","cauim","6",1765
"vtoclga","cauim","9",1766
"fveq2","cauim","10",1767
"fveq2","cauim","11",1768
"vtoclga","cauim","14",1769
"opreq2","serabsdiflem","13",1770
"opreq2","serabsdiflem","17",1771
"fveq2","sercj","8",1772
"fveq2","sercj","9",1773
"fveq2","facclt","3",1774
"opreq2","faclbnd","5",1775
"fveq2","faclbnd","7",1776
"breq2","facdivt","7",1777
"fveq2","facdivt","8",1778
"climuni","climmo","3",1779
"breq2","climmo","5",1780
"breq2","climshift","96",1781
"fveq2","climshift","97",1782
"opreq1","climshift","98",1783
"rcla4v","climshift","102",1784
"fveq2","climre","8",1785
"fveq2","climre","9",1786
"vtoclga","climre","12",1787
"fveq2","climre","35",1788
"fveq2","climre","36",1789
"vtoclga","climre","39",1790
"fveq2","climre","55",1791
"fveq2","climre","56",1792
"vtoclga","climre","59",1793
"breq2","climrecl","76",1794
"fveq2","climrecl","77",1795
"rcla4ev","climrecl","83",1796
"breq2","climadd","100",1797
"fveq2","climadd","101",1798
"rcla4v","climadd","107",1799
"fveq2","climadd","173",1800
"fveq2","climadd","174",1801
"fveq2","climadd","175",1802
"vtoclga","climadd","178",1803
"fveq2","climadd","214",1804
"fveq2","climadd","215",1805
"fveq2","climadd","216",1806
"vtoclga","climadd","219",1807
"eleq1","climaconstOLD","8",1808
"fveq2","climaconstOLD","9",1809
"fveq2","climaconstOLD","10",1810
"eleq1","climmconst","6",1811
"fveq2","climmconst","7",1812
"fveq2","climmconst","8",1813
"eleq1","climmconst","29",1814
"fveq2","climmconst","30",1815
"fveq2","climmconst","31",1816
"eleq1","climmconst","100",1817
"fveq2","climmconst","101",1818
"fveq2","climmconst","102",1819
"eleq1","climmconst","153",1820
"fveq2","climmconst","154",1821
"fveq2","climmconst","155",1822
"breq2","climcau","27",1823
"fveq2","climcau","28",1824
"rcla4v","climcau","33",1825
"breq2","climcau","49",1826
"fveq2","climcau","50",1827
"rcla4v","climcau","55",1828
"breq2","caucvglem2","42",1829
"fveq2","caucvglem2","43",1830
"rcla4v","caucvglem2","46",1831
"fveq2","caucvglem2","49",1832
"rcla4v","caucvglem2","52",1833
"breq2","caucvg","170",1834
"fveq2","caucvg","171",1835
"rcla4v","caucvg","176",1836
"fveq2","ser0","3",1837
"fveq2","sertrunclem","11",1838
"breq1","sertrunclem","12",1839
"opreq1","sertrunclem","14",1840
"breq1","sertrunc2","18",1841
"fvopab4","sertrunc2","25",1842
"fveq2","sercmp","7",1843
"fveq2","sercmp","8",1844
"fveq2","sercmp2","11",1845
"fveq2","sercmp2","12",1846
"fveq2","cvgcmp2lem","73",1847
"fveq2","cvgcmp2lem","74",1848
"vtoclga","cvgcmp2lem","77",1849
"fveq2","cvgcmp2","13",1850
"fvopab4","cvgcmp2","17",1851
"fveq2","cvgcmp2c","14",1852
"fvopab4","cvgcmp2c","18",1853
"fveq2","cvgcmp3ce","13",1854
"fvopab4","cvgcmp3ce","17",1855
"fveq2","cvgcmp3ce","21",1856
"fvopab4","cvgcmp3ce","25",1857
"fveq2","cvgcmp3ce","30",1858
"fvopab4","cvgcmp3ce","34",1859
"fveq2","cvgcmp3ce","39",1860
"fvopab4","cvgcmp3ce","43",1861
"fveq2","cvgcmp3cetlem1","10",1862
"vtoclga","cvgcmp3cetlem1","12",1863
"breq2","cvgcmp3cetlem1","21",1864
"fveq2","cvgcmp3cetlem1","22",1865
"fveq2","cvgcmp3cetlem1","24",1866
"breq2","cvgcmp3cetlem1","100",1867
"fveq2","cvgcmp3cetlem1","101",1868
"fveq2","cvgcmp3cetlem1","103",1869
"breq2","cvgcmp3cetlem1","179",1870
"fveq2","cvgcmp3cetlem1","180",1871
"fveq2","cvgcmp3cetlem1","182",1872
"breq2","cvgcmp3cetlem1","258",1873
"fveq2","cvgcmp3cetlem1","259",1874
"fveq2","cvgcmp3cetlem1","261",1875
"fveq2","cvgcmp3cetlem2","23",1876
"fveq2","cvgcmp3cetlem2","72",1877
"fveq2","cvgcmp3cetlem2","122",1878
"breq2","cvgcmp3cetlem2","165",1879
"fveq2","cvgcmp3cetlem2","166",1880
"fveq2","cvgcmp3cetlem2","168",1881
"opreq2","expcnv","10",1882
"fvopab4","expcnv","12",1883
"opreq2","expcnv","31",1884
"fvopab4","expcnv","33",1885
"fveq2","geoser","44",1886
"opreq1","geoser","46",1887
"opreq2","geolimilem","264",1888
"fvopab4","geolimilem","266",1889
"opreq2","geolimi","7",1890
"fvopab4","geolimi","11",1891
"opreq2","geolimi","12",1892
"fvopab4","geolimi","14",1893
"opreq2","cvgratlem1","8",1894
"opreq2","cvgratlem1","10",1895
"fveq2","cvgratlem3","32",1896
"fvopab4","cvgratlem3","35",1897
"opreq2","cvgratlem5","23",1898
"fvopab4","cvgratlem5","25",1899
"opreq2","cvgratlem5","81",1900
"fvopab4","cvgratlem5","83",1901
"climuni","sumclt","9",1902
"eleq1","sumclt","15",1903
"breq2","sumclt","16",1904
"opreq2","efcltlem1","346",1905
"fveq2","efcltlem1","347",1906
"fvopab4","efcltlem1","350",1907
"opreq2","erelem2","89",1908
"fvopab4","erelem2","92",1909
"opreq2","erelem2","93",1910
"fvopab4","erelem2","96",1911
"fveq2","erelem3","31",1912
"fvopab4","erelem3","34",1913
"fveq2","erelem3","127",1914
"fvopab4","erelem3","130",1915
"opreq2","erelem3","131",1916
"fvopab4","erelem3","134",1917
"eleq1","ruclem12","2",1918
"eleq1","ruclem12","4",1919
"ruclem4","ruclem12","7",1920
"eqeq1","ruclem12","11",1921
"eqid","ruclem15","23",1922
"ruclem4","ruclem15","24",1923
"fveq2","ruclem25","10",1924
"fveq2","ruclem25","11",1925
"opreq2","ruclem32","11",1926
"opreq1","ruclem32","50",1927
"nn0opth2t","xpnnen","60",1928
"eqeq12","xpnnen","69",1929
"opth","xpnnen","73",1930
"ltnet","znnenlem","14",1931
"mulcant2","znnen","66",1932
"mulcant2","znnen","114",1933
"om2uzlt2","unbenlem","34",1934
"breq2","infpnlem2","46",1935
"opreq2","infpnlem2","47",1936
"infpnlem1","infpnlem2","52",1937
"breq2","infpn","22",1938
"opreq1","infpn","23",1939
"eqeq2","infpn","25",1940
"elrab","infpn","30",1941
"breq2","infxpidmlem2","9",1942
"sseq1","infxpidmlem2","10",1943
"xpeq1","infxpidmlem2","12",1944
"xpeq2","infxpidmlem2","13",1945
"f1oeq3","infxpidmlem2","17",1946
"sseq1","infxpidmlem7","55",1947
"sseq2","infxpidmlem7","56",1948
"sseq2","infxpidmlem7","58",1949
"sseq1","infxpidmlem7","59",1950
"rcla42v","infxpidmlem7","61",1951
"psseq2","infxpidmlem10","7",1952
"rcla4v","infxpidmlem10","9",1953
"sseq1","infmap2lem1","8",1954
"breq1","infmap2lem1","9",1955
"foeq3","infmap2lem1","11",1956
"opelopab","infmap2lem1","15",1957
"sseq1","infmap2lem1","41",1958
"breq1","infmap2lem1","42",1959
"eqeqan12d","infmap2lem2","55",1960
"fveq2","infmap2lem2","58",1961
"eleq2","closedsub","7",1962
"breq2","hlimcaui","72",1963
"fveq2","hlimcaui","73",1964
"hlimuni","hlimreu","4",1965
"breq2","hlimreu","8",1966
"hlimuni","hlimeu","4",1967
"breq2","hlimeu","7",1968
"df-rex","chsscm","13",1969
"closedsub","chsscm","23",1970
"df-rex","chcmh","19",1971
"closedsub","chcmh","35",1972
"eleq1","ch2","10",1973
"feq3","ch2","11",1974
"rexeq","ch2","12",1975
"opreq2","ocin","2",1976
"rcla4v","ocin","4",1977
"fveq2","occllem5","2",1978
"rcla4v","occllem5","5",1979
"eqeq1","projlem8","28",1980
"elrab","projlem8","30",1981
"opreq1","projlem10","16",1982
"rcla4ev","projlem10","20",1983
"eqeq1","projlem13","14",1984
"elrab","projlem13","16",1985
"eqeq1","projlem15","55",1986
"opreq1","projlem15","57",1987
"elrab","projlem15","63",1988
"opreq2","projlem26","99",1989
"fveq2","projlem26","101",1990
"fveq2","projlem26","105",1991
"opreq2","projlem26","108",1992
"rcla4v","projlem26","112",1993
"opreq2","projlem26","153",1994
"fveq2","projlem26","155",1995
"fveq2","projlem26","159",1996
"opreq2","projlem26","162",1997
"rcla4v","projlem26","166",1998
"chocuni","pjthu","4",1999
"opreq2","pjthu","12",2000
"opreq1","pjthu","25",2001
"chocuni","pjthu2","6",2002
"opreq1","pjthu2","14",2003
"opreq2","pjthu2","27",2004
"eleq2","pjmvalt","1",2005
"df-rab","pjmvalt","7",2006
"elinti","shintcl","23",2007
"elinti","shintcl","25",2008
"shaddclt","shintcl","30",2009
"elinti","shintcl","39",2010
"shmulclt","shintcl","44",2011
"chlim","chintcl","12",2012
"elint2","chintcl","21",2013
"opreq1","shunss","3",2014
"rcla42ev","shunss","7",2015
"opreq2","shunss","18",2016
"rcla42ev","shunss","20",2017
"elspan","spanun","40",2018
"elspan","spanun","43",2019
"shaddclt","spanun","52",2020
"eleq1","spanun","54",2021
"elspan","spanun","62",2022
"eleq1a","spansn","8",2023
"elspan","spansn","24",2024
"feq1","hosmvalt","19",2025
"elab","hosmvalt","20",2026
"feq1","hosmvalt","22",2027
"elab","hosmvalt","23",2028
"feq1","hodmvalt","19",2029
"elab","hodmvalt","20",2030
"feq1","hodmvalt","22",2031
"elab","hodmvalt","23",2032
"eqeq2d","spansncv","53",2033
"eleq1a","spansncv","54",2034
"fveq2","pjjs","3",2035
"rcla4v","pjjs","5",2036
"eleq1","pjrn","8",2037
"fveq2","pjrn","9",2038
"cla4ev","pjrn","12",2039
"fveq2","hun","3",2040
"opreq1","hun","5",2041
"fveq2","hun","7",2042
"opreq2","hun","9",2043
"hvsubeq0t","hun1o","48",2044
"sseq1","mdbr3","26",2045
"opreq1","mdbr3","27",2046
"opreq1","mdbr3","29",2047
"sseq1","mdbr4","26",2048
"opreq1","mdbr4","27",2049
"opreq1","mdbr4","29",2050
"sseq2","dmdbr3","29",2051
"ineq1","dmdbr3","30",2052
"ineq1","dmdbr3","32",2053
"sseq2","dmdbr4","29",2054
"ineq1","dmdbr4","30",2055
"ineq1","dmdbr4","31",2056
"breq2","mddmd","20",2057
"sseq1","hatomistic","10",2058
"elrab","hatomistic","11",2059
"sseq1","hatomistic","12",2060
"elrab","hatomistic","13",2061
"sseq1","hatomistic","26",2062
"elrab","hatomistic","27",2063
"opreq1","mdsymlem2","4",2064
"sseq1","mdsymlem2","6",2065
"rcla4ev","mdsymlem2","9",2066
"atnem0","mdsymlem3","33",2067
"sseq1","mdsymlem3","35",2068
"atnem0","mdsymlem5","4",2069
"sseq1","mdsymlem6","5",2070
"shsubclt","sumdmdi","6",2071
"ssel2","sumdmdi","9",2072
"chelt","sumdmdi","24",2073
"eleq1","sumdmdi","30",2074
"elin","sumdmdi","41",2075
"elin","sumdmdi","64",2076
"eqeq2d","sumdmdlem","41",2077
"eleq1","sumdmdlem","47",2078