A Universe of Sorts

Theorem: Every bijective bounded linear operator has bounded inverse.
Equivaently: Every bijective continuous linear operator has continuous inverse.
Proof: quick corollary of open mapping. Let $L: X \to Y$ be bijective bounded linear operator.
Assuming open mapping, we know that $T$ maps opens $U$ to open sets. Recall that bounded iff continuous. Thus, we can show that $T \equiv L^{-1} : Y \to X$ is continuous to show that $L$ is bounded.
We need to show that inverse images of open sets under $T$ is open. Specifically that $T^{-1}(U \subseteq X)$ is open for $U$ open
Since $V \equiv L(U)$ is open as $U$ is open and $L$ is an open map, this means that $V \equiv T^{-1}(U)$ is open, as $L = T^{-1}$ . Hence done.

§ Bounded Inverse Theorem