Set Theory 2: The Two Functions

Working on importing chapter 2 of Jech's Set Theory.

Changes and additions:

⚙ functions are now implemented as being in the set ->(x, y) ➕ function application (changed def!)

app(f, x) = z such that (functional(f) /\ x \in dom(f) ==> (x, z) \in f) /\ (!functional(f) \/ ! x \in dom(f) ==> (z = emptySet()))

➕ injective, surjective, bijective functions 〰 [WIP] invertible functions and uniqueness ⚙ Changed partial orders to be a pair (x, r) ➕ order preserving functions and isomorphisms of partial orders

Saved for later: ❓ Well-Orders ❓ Order-types ❓ Ordinals ❗ ❗ ❗ ❓ Transfinite Recursion ❓ Ordinal Arithmetic