The first Chern class classifies complex line bundles

The numerable circle bundle [F5] is a Serre fibration by [F6]. Its total space is contractible, so exactness between the two zero total-space groups gives ${\pi }_k({\mathbb{C}\mathbb{P}}^{\mathrm{\infty }})\cong {\pi }_{k-1}(S^1)$ for $k\ge 2$. In degree one the segment $0\to {\pi }_1(B{S}^1)\to {\pi }_0(S^1)$ and connectedness of $S^1$ give zero fundamental group. The base is path connected as the image of the nonempty contractible total space under its surjective bundle projection. By [F4], the circle has only ${\pi }_1=\mathbb{Z}$ nonzero, hence ${\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}$ is a CW model of $K(\mathbb{Z},2)$, marked by the connecting isomorphism.

The universal class $c_1(\gamma )$ equals $e({\gamma }_{\mathbb{R}})$ by [F2], using the complex orientation of the tautological line. By [F7] this is a generator of $H^2({\mathbb{C}\mathbb{P}}^{\mathrm{\infty }};\mathbb{Z})\cong \mathbb{Z}$.

By [F3] applied to the $K(\mathbb{Z},2)$ model ${\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}$ of step 1.1, pullback of the fundamental class gives a natural bijection $[X,{\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}{]}_{\ast }\cong H^2(X;\mathbb{Z})$; by step 1.2 the fundamental class is $\pm c_1(\gamma )$, so $f\mapsto f^{\ast }{c}_1(\gamma )$ is also a natural bijection.

To pass from based to unbased classes, any map $f:X\to {\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}$ can be made based by a homotopy: choose a path from $f(x_0)$ to the target vertex and extend this homotopy of the vertex over $X$ using [F10]. If two based maps are freely homotopic, their pullbacks of $c_1(\gamma )$ agree by [F10], so step 2.1 says their based homotopy classes already agree. Hence forgetting the basepoint is a bijection, and the unbased map $[f]\mapsto f^{\ast }{c}_1(\gamma )$ is bijective as well. Composing with [F1] and using line naturality [F2] proves that $L\mapsto c_1(L)$ is a natural bijection.

Additivity. On ${\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}\times {\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}$ let $q_i$ be the projections and $L=q_1^{\ast }\gamma \otimes q_2^{\ast }\gamma$. By [F8] one has $H^2({\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}\times {\mathbb{C}\mathbb{P}}^{\mathrm{\infty }};\mathbb{Z})=\mathbb{Z}(u\otimes 1)\oplus \mathbb{Z}(1\otimes u)$ with $u=c_1(\gamma )$ a generator; line naturality [F2] gives $c_1(L){\mathrm{\mid }}_{{\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}\times \{\ast \}}=u=c_1(L){\mathrm{\mid }}_{\{\ast \}\times {\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}}$, so $c_1(L)=u\otimes 1+1\otimes u$. For arbitrary numerable lines $L_i=f_i^{\ast }\gamma$ classified by maps $f_i$, the identity $L_1\otimes L_2=(f_1,f_2{)}^{\ast }L$ and naturality give $c_1(L_1\otimes L_2)=(f_1,f_2{)}^{\ast }(u\otimes 1+1\otimes u)=c_1(L_1)+c_1(L_2)$.

The tensor unit is the trivial line, and evaluation gives $L\otimes L^{\ast }\cong {\epsilon }^1$, so these bundle classes form a group by [F9]. The bijection in step 3.1 preserves multiplication by step 4.1 and is therefore a group isomorphism. For a path-connected paracompact Hausdorff CGWH space $Y$ of CW type, choose a homotopy equivalence $h:X\to Y$ from a CW complex with vertex basepoint. Precomposition with $h$ is bijective on unbased homotopy classes of maps into ${\mathbb{C}\mathbb{P}}^{\mathrm{\infty }}$, so [F1] makes $h^{\ast }$ bijective on line-bundle classes; it respects tensor products by [F9]. It is an isomorphism on cohomology by [F10]. Naturality [F2] makes the square of these two pullbacks with $c_1$ commute. The already proved isomorphism for $X$ therefore proves the asserted isomorphism for $Y$. This also proves naturality for maps between the allowed CW-type bases.

Boundary cases. For $X$ a point the statement reads that the only line bundle is trivial and $H^2(\ast ;\mathbb{Z})=0$, both true. The trivial line has $c_1=0$ because both are groups and the trivial bundle is the unit; the dual satisfies $c_1(L^{\ast })=-c_1(L)$ by the group law. The coefficient ring $\mathbb{Z}$ is nonzero, and the empty space is excluded by the path-connected hypothesis. AC is used through [A1]: besides classification, representability, the numerable-fibration theorem and the Euler-class supplier, step 1.2 uses the AC-qualified computation [F7] and step 4.1 uses the AC-qualified Kunneth isomorphism [F8]. No additional choice of orientations or lifts is made in this proof.