Metamath Proof Explorer


Table of Contents - 20.35.3.1. Grothendieck universes are closed under collection

  1. gru0eld
  2. grusucd
  3. r1rankcld
  4. grur1cld
  5. grurankcld
  6. grurankrcld
  7. cscott
  8. df-scott
  9. scotteqd
  10. scotteq
  11. nfscott
  12. scottabf
  13. scottab
  14. scottabes
  15. scottss
  16. elscottab
  17. scottex2
  18. scotteld
  19. scottelrankd
  20. scottrankd
  21. gruscottcld
  22. ccoll
  23. df-coll
  24. dfcoll2
  25. colleq12d
  26. colleq1
  27. colleq2
  28. nfcoll
  29. collexd
  30. cpcolld
  31. cpcoll2d
  32. grucollcld