Every Planar Graph Is 5-Choosable

We prove the statement of the title, which was conjectured in 1975 by V. G. Vizing and, independently, in 1979 by P. Erdِs, A. L. Rubin, and H Taylor.