Metamath Proof Explorer

Table of Contents - 2.4.33. Ordinal isomorphism, Hartogs's theorem

  1. coi
  2. df-oi
  3. dfoi
  4. oieq1
  5. oieq2
  6. nfoi
  7. ordiso2
  8. ordiso
  9. ordtypecbv
  10. ordtypelem1
  11. ordtypelem2
  12. ordtypelem3
  13. ordtypelem4
  14. ordtypelem5
  15. ordtypelem6
  16. ordtypelem7
  17. ordtypelem8
  18. ordtypelem9
  19. ordtypelem10
  20. oi0
  21. oicl
  22. oif
  23. oiiso2
  24. ordtype
  25. oiiniseg
  26. ordtype2
  27. oiexg
  28. oion
  29. oiiso
  30. oien
  31. oieu
  32. oismo
  33. oiid
  34. hartogslem1
  35. hartogslem2
  36. hartogs
  37. wofib
  38. wemaplem1
  39. wemaplem2
  40. wemaplem3
  41. wemappo
  42. wemapsolem
  43. wemapso
  44. wemapso2lem
  45. wemapso2
  46. card2on
  47. card2inf