Metamath Proof Explorer

Table of Contents - 4.1. Inaccessibles

Weakly and strongly inaccessible cardinals
1. cwina
2. cina
3. df-wina
4. df-ina
5. elwina
6. elina
7. winaon
8. inawinalem
9. inawina
10. omina
11. winacard
12. winainflem
13. winainf
14. winalim
15. winalim2
16. winafp
17. winafpi
18. gchina
Weak universes
1. cwun
2. cwunm
3. df-wun
4. df-wunc
5. iswun
6. wuntr
7. wununi
8. wunpw
9. wunelss
10. wunpr
11. wunun
12. wuntp
13. wunss
14. wunin
15. wundif
16. wunint
17. wunsn
18. wunsuc
19. wun0
20. wunr1om
21. wunom
22. wunfi
23. wunop
24. wunot
25. wunxp
26. wunpm
27. wunmap
28. wunf
29. wundm
30. wunrn
31. wuncnv
32. wunres
33. wunfv
34. wunco
35. wuntpos
36. intwun
37. r1limwun
38. r1wunlim
39. wunex2
40. wunex
41. uniwun
42. wunex3
43. wuncval
44. wuncid
45. wunccl
46. wuncss
47. wuncidm
48. wuncval2
Tarski classes
1. ctsk
2. df-tsk
3. eltskg
4. eltsk2g
5. tskpwss
6. tskpw
7. tsken
8. 0tsk
9. tsksdom
10. tskssel
11. tskss
12. tskin
13. tsksn
14. tsktrss
15. tsksuc
16. tsk0
17. tsk1
18. tsk2
19. 2domtsk
20. tskr1om
21. tskr1om2
22. tskinf
23. tskpr
24. tskop
25. tskxpss
26. tskwe2
27. inttsk
28. inar1
29. r1omALT
30. rankcf
31. inatsk
32. r1omtsk
33. tskord
34. tskcard
35. r1tskina
36. tskuni
37. tskwun
38. tskint
39. tskun
40. tskxp
41. tskmap
42. tskurn
Grothendieck universes
1. cgru
2. df-gru
3. elgrug
4. grutr
5. gruelss
6. grupw
7. gruss
8. grupr
9. gruurn
10. gruiun
11. gruuni
12. grurn
13. gruima
14. gruel
15. grusn
16. gruop
17. gruun
18. gruxp
19. grumap
20. gruixp
21. gruiin
22. gruf
23. gruen
24. gruwun
25. intgru
26. ingru
27. wfgru
28. grudomon
29. gruina
30. grur1a
31. grur1
32. grutsk1
33. grutsk