# Metamath Proof Explorer

1. Introduce the Axiom of Union
2. Ordinals (continued)
3. Transfinite induction
4. The natural numbers (i.e., finite ordinals)
5. Peano's postulates
6. Finite induction (for finite ordinals)
7. Relations and functions (cont.)
8. First and second members of an ordered pair
9. The support of functions
10. Special maps-to operations
11. Function transposition
12. Curry and uncurry
13. Undefined values
14. Well-founded recursion
15. Functions on ordinals; strictly monotone ordinal functions
16. "Strong" transfinite recursion
17. Recursive definition generator
18. Finite recursion
19. Ordinal arithmetic
20. Natural number arithmetic
21. Equivalence relations and classes
22. The mapping operation
23. Infinite Cartesian products
24. Equinumerosity
25. Schroeder-Bernstein Theorem
26. Equinumerosity (cont.)
27. Pigeonhole Principle
28. Finite sets
29. Finitely supported functions
30. Finite intersections
31. Hall's marriage theorem
32. Supremum and infimum
33. Ordinal isomorphism, Hartogs's theorem
34. Hartogs function
35. Weak dominance