From my perspective, the development of axiom systems such as ZF is an important part of mathematics. That is where much of the creativity and inventiveness is needed. By looking at only proofs derived from axioms, and ignoring the origin of the axiom systems, you omit some of what I consider to be the most important parts of mathematics.
But this is, in part, what considering different topoi is all about. And it's not exactly an inactive area of research...
You first have to introduce new concepts, new definitions, new axioms (such as the defining axioms of a Banach space).
What makes you think we can't build Banach spaces from ZF? Not that I've ever tried
but there's nothing especially exotic about a Banach space.
Ph.D. was related to fixed point properies on topological groups.
Cool! My life seemed to revolve around topological groups for several years (though usually Lie groups in my case).