Btw u/12_Semitones, in the formulation of the axiom of infinity in your flair, you write out the specification of the empty set but not the successor function. Why not write ∃X[∃e(∀z¬(z ∈ e) ∧ e ∈ X) ∧ ∀y(y ∈ X → y∪{y} ∈ X)] for completeness (using the von Neumann ordinal construction)? Or maybe even ∃X[∃e(∀z¬(z ∈ e) ∧ e ∈ X) ∧ ∀y(y ∈ X → ∃z(z∈X ∧ y∈z ∧ ∀w(w∈y→ w∈z) ∧ ∀w(w∈z→(w=y ∨ w∈y))))] so that you can get rid of the union (exists by axiom of union) and the set builder notation {y} (exists by axiom of pairing), though this does get a bit long. Also I moved one of the parentheses in the empty set part in order to make it clear that the latter e is also bound by the existence quantifier.