Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
∈ wcel 2107 Ord word 6364
Oncon0 6365 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-ral 3063 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-tr 5267 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-ord 6368 df-on 6369 |
This theorem is referenced by: oneli
6479 ssorduni
7766 unon
7819 tfindsg2
7851 dfom2
7857 trom
7864 onfununi
8341 onnseq
8344 dfrecs3
8372 dfrecs3OLD
8373 tz7.48-2
8442 tz7.49
8445 oalim
8532 omlim
8533 oelim
8534 oaordi
8546 oalimcl
8560 oaass
8561 omordi
8566 omlimcl
8578 odi
8579 omass
8580 omeulem1
8582 omeulem2
8583 omopth2
8584 oewordri
8592 oeordsuc
8594 oelimcl
8600 oeeui
8602 oaabs2
8648 omabs
8650 naddssim
8684 naddel12
8699 omxpenlem
9073 hartogs
9539 card2on
9549 cantnfle
9666 cantnflt
9667 cantnfp1lem3
9675 cantnfp1
9676 oemapvali
9679 cantnflem1b
9681 cantnflem1c
9682 cantnflem1d
9683 cantnflem1
9684 cantnflem2
9685 cantnflem3
9686 cantnflem4
9687 cantnf
9688 cnfcomlem
9694 cnfcom3lem
9698 cnfcom3
9699 r1ordg
9773 r1val3
9833 tskwe
9945 iscard
9970 cardmin2
9994 infxpenlem
10008 infxpenc2lem2
10015 alephordi
10069 alephord2i
10072 alephle
10083 cardaleph
10084 cfub
10244 cfsmolem
10265 zorn2lem5
10495 zorn2lem6
10496 ttukeylem6
10509 ttukeylem7
10510 ondomon
10558 cardmin
10559 alephval2
10567 alephreg
10577 smobeth
10581 winainflem
10688 inar1
10770 inatsk
10773 sltval2
27159 sltres
27165 nosepeq
27188 nosupno
27206 nosupres
27210 nosupbnd1lem1
27211 nosupbnd2lem1
27218 nosupbnd2
27219 noinfno
27221 noinfres
27225 noinfbnd1lem1
27226 noinfbnd2lem1
27233 noinfbnd2
27234 oldlim
27381 oldbday
27395 dfrdg2
34767 dfrdg4
34923 ontopbas
35313 onpsstopbas
35315 onint1
35334 onelord
42000 cantnfresb
42074 oawordex2
42076 oacl2g
42080 omabs2
42082 omcl2
42083 tfsconcatfv2
42090 tfsconcatfv
42091 tfsconcatrn
42092 tfsconcat0i
42095 ofoafg
42104 ofoaass
42110 oaun3lem1
42124 oaun3lem2
42125 oadif1lem
42129 oadif1
42130 nadd2rabtr
42134 nadd1suc
42142 naddsuc2
42143 naddgeoa
42145 naddwordnexlem0
42147 naddwordnexlem1
42148 naddwordnexlem3
42150 oawordex3
42151 naddwordnexlem4
42152 omssrncard
42291 |