Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2106
Ord word 6363 Oncon0 6364 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-v 3476 df-in 3955 df-ss 3965 df-uni 4909 df-tr 5266 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-ord 6367 df-on 6368 |
This theorem is referenced by: onelon
6389 onin
6395 ontri1
6398 onfr
6403 onelpss
6404 onsseleq
6405 onelss
6406 ontr1
6410 ontr2
6411 ordunidif
6413 on0eln0
6420 ordsssuc
6453 onsssuc
6454 onnbtwn
6458 onunel
6469 suc11
6471 onun2
6472 ontr
6473 onordi
6475 onssneli
6480 epweon
7764 epweonALT
7765 ordeleqon
7771 onss
7774 sucexeloni
7799 ordsucOLD
7804 onpwsuc
7806 onpsssuc
7809 onsucmin
7811 ordunpr
7816 ordunisuc
7822 onsucuni2
7824 onuniorsuc
7827 ordunisuc2
7835 ordzsl
7836 onzsl
7837 nlimon
7842 tfinds
7851 tfindsg2
7853 nnord
7865 poseq
8146 soseq
8147 onfununi
8343 smo11
8366 smoord
8367 smoword
8368 smogt
8369 tfrlem1
8378 tfrlem9a
8388 tfrlem15
8394 tz7.44-2
8409 tz7.48lem
8443 ord3
8485 oe0m1
8523 oaordi
8548 oaord
8549 oacan
8550 oawordri
8552 oalimcl
8562 oaass
8563 omord2
8569 omcan
8571 omwordi
8573 omword1
8575 omword2
8576 om00
8577 omlimcl
8580 omass
8582 omeulem2
8585 omopth2
8586 oen0
8588 oeord
8590 oecan
8591 oewordi
8593 oeworde
8595 oelimcl
8602 oeeulem
8603 oeeui
8604 nnarcl
8618 nnawordi
8623 nnawordex
8639 oaabs2
8650 omabs
8652 omsmo
8659 cofonr
8675 naddcllem
8677 omxpenlem
9075 infensuc
9157 dif1enlem
9158 nndomog
9218 nndomogOLD
9228 onomeneq
9230 onomeneqOLD
9231 ordiso
9513 ordtypelem2
9516 hartogslem1
9539 cantnflt
9669 cantnfp1lem3
9677 cantnfp1
9678 oemapso
9679 oemapvali
9681 cantnflem1d
9685 cantnflem1
9686 cantnf
9690 oemapwe
9691 cantnffval2
9692 cnfcom
9697 r111
9772 r1ordg
9775 rankonidlem
9825 bndrank
9838 r1pw
9842 r1pwALT
9843 rankbnd2
9866 tcrank
9881 cardprclem
9976 carduni
9978 cardmin2
9996 infxpenlem
10010 alephdom
10078 alephdom2
10084 cardaleph
10086 iscard3
10090 alephfp
10105 dfac12lem1
10140 dfac12lem2
10141 dfac12lem3
10142 cflim2
10260 cofsmo
10266 cfsmolem
10267 coftr
10270 cfcof
10271 fin67
10392 hsmexlem5
10427 zorn2lem6
10498 ttukeylem3
10508 ttukeylem5
10510 ttukeylem6
10511 ttukeylem7
10512 winainflem
10690 r1limwun
10733 r1wunlim
10734 tsksuc
10759 inar1
10772 gruina
10815 grur1a
10816 grur1
10817 nodmord
27380 noextendseq
27394 noextenddif
27395 nosupno
27430 nosupbday
27432 nosupres
27434 noinfno
27445 noinfbday
27447 noinfres
27449 noetasuplem4
27463 noetainflem4
27467 newbday
27621 dfrdg2
35059 ontgval
35619 ontgsucval
35620 onsuctopon
35622 onintopssconn
35628 onsuct0
35629 sucneqond
36549 onsucuni3
36551 aomclem4
42101 aomclem5
42102 onintunirab
42278 omlimcl2
42293 onelord
42302 oneltri
42309 ordeldifsucon
42311 ordeldif1o
42312 onsucss
42318 onsucf1olem
42322 onov0suclim
42326 oe0rif
42337 onsucwordi
42340 oege1
42358 cantnfresb
42376 omabs2
42384 ordsssucb
42387 tfsconcatlem
42388 tfsconcatfv2
42392 tfsconcatrn
42394 tfsconcatb0
42396 tfsconcat0b
42398 tfsconcatrev
42400 onsucunipr
42424 oaun3lem1
42426 oaun3lem2
42427 nadd1suc
42444 naddsuc2
42445 naddgeoa
42447 oaltom
42458 omltoe
42460 nlimsuc
42494 dfsucon
42576 minregex
42587 onfrALTlem3
43607 onfrALTlem2
43609 onfrALTlem3VD
43950 onfrALTlem2VD
43952 onsetreclem3
47840 |