Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
∈ wcel 2107 Ord word 6321
Oncon0 6322 |
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 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
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 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-ral 3066 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-tr 5228 df-eprel 5542 df-po 5550 df-so 5551 df-fr 5593 df-we 5595 df-ord 6325 df-on 6326 |
This theorem is referenced by: oneli
6436 ssorduni
7718 unon
7771 tfindsg2
7803 dfom2
7809 trom
7816 onfununi
8292 onnseq
8295 dfrecs3
8323 dfrecs3OLD
8324 tz7.48-2
8393 tz7.49
8396 oalim
8483 omlim
8484 oelim
8485 oaordi
8498 oalimcl
8512 oaass
8513 omordi
8518 omlimcl
8530 odi
8531 omass
8532 omeulem1
8534 omeulem2
8535 omopth2
8536 oewordri
8544 oeordsuc
8546 oelimcl
8552 oeeui
8554 oaabs2
8600 omabs
8602 naddssim
8636 naddel12
8651 omxpenlem
9024 hartogs
9487 card2on
9497 cantnfle
9614 cantnflt
9615 cantnfp1lem3
9623 cantnfp1
9624 oemapvali
9627 cantnflem1b
9629 cantnflem1c
9630 cantnflem1d
9631 cantnflem1
9632 cantnflem2
9633 cantnflem3
9634 cantnflem4
9635 cantnf
9636 cnfcomlem
9642 cnfcom3lem
9646 cnfcom3
9647 r1ordg
9721 r1val3
9781 tskwe
9893 iscard
9918 cardmin2
9942 infxpenlem
9956 infxpenc2lem2
9963 alephordi
10017 alephord2i
10020 alephle
10031 cardaleph
10032 cfub
10192 cfsmolem
10213 zorn2lem5
10443 zorn2lem6
10444 ttukeylem6
10457 ttukeylem7
10458 ondomon
10506 cardmin
10507 alephval2
10515 alephreg
10525 smobeth
10529 winainflem
10636 inar1
10718 inatsk
10721 sltval2
27020 sltres
27026 nosepeq
27049 nosupno
27067 nosupres
27071 nosupbnd1lem1
27072 nosupbnd2lem1
27079 nosupbnd2
27080 noinfno
27082 noinfres
27086 noinfbnd1lem1
27087 noinfbnd2lem1
27094 noinfbnd2
27095 oldlim
27238 oldbday
27252 dfrdg2
34409 dfrdg4
34565 ontopbas
34929 onpsstopbas
34931 onint1
34950 onelord
41614 cantnfresb
41688 oawordex2
41690 oacl2g
41694 omabs2
41696 omcl2
41697 ofoafg
41699 ofoaass
41705 oaun3lem1
41719 oaun3lem2
41720 oadif1lem
41724 oadif1
41725 nadd2rabtr
41729 nadd1suc
41737 naddsuc2
41738 naddgeoa
41740 naddwordnexlem0
41742 naddwordnexlem1
41743 naddwordnexlem3
41745 oawordex3
41746 naddwordnexlem4
41747 omssrncard
41886 |