[proofplan] The equivariant map $f:X \to Y$ induces a continuous map between orbit spaces. The quotient double cover $q_X:X \to X/(\mathbb Z/2)$ is the pullback of $q_Y:Y \to Y/(\mathbb Z/2)$ along that induced map, so naturality of the first Stiefel-Whitney class gives $\bar f^*(w_Y)=w_X$. Since pullback in cohomology preserves cup products, every nonzero power of $w_X$ is the pullback of the corresponding power of $w_Y$, forcing that power of $w_Y$ to be nonzero. Taking the supremum over all such powers gives the desired inequality. [/proofplan]

[step:Descend the equivariant map to orbit spaces] Let $G := \mathbb Z/2$. Define the orbit-space map \begin{align*} \bar f:X/G \to Y/G,\qquad \bar f([x]) = [f(x)]. \end{align*} This is well-defined: if $[x]=[x']$ in $X/G$, then there exists $g \in G$ such that $x'=g \cdot x$, and equivariance of $f$ gives \begin{align*} f(x') = f(g \cdot x)=g \cdot f(x), \end{align*} so $[f(x')]=[f(x)]$ in $Y/G$. Since the quotient maps $q_X:X \to X/G$ and $q_Y:Y \to Y/G$ are quotient maps and \begin{align*} \bar f \circ q_X = q_Y \circ f, \end{align*} the [universal property of the quotient topology](/theorems/1031) implies that $\bar f$ is continuous. [/step]

[step:Identify the pulled-back double cover]By the strengthened hypothesis, $q_X:X \to X/G$ and $q_Y:Y \to Y/G$ are double covers. Define the pullback total space \begin{align*} P=\{([x],y)\in (X/G)\times Y:\bar f([x])=q_Y(y)\} \end{align*} and let $\pi:P\to X/G$ be the map $\pi([x],y)=[x]$. The pullback cover $\bar f^*q_Y$ is precisely $\pi:P\to X/G$. Define \begin{align*} \Phi:X \to P, \end{align*} by $\Phi(x)=([x],f(x))$. This is well-defined as a map into $P$ because $q_Y(f(x))=[f(x)]=\bar f([x])$, and it is continuous because both $q_X$ and $f$ are continuous and $P$ has the [subspace topology](/page/Subspace%20Topology) from $(X/G)\times Y$. Moreover $\pi\circ\Phi=q_X$, so $\Phi$ is a morphism over $X/G$. We prove that $\Phi$ is a homeomorphism of double covers by checking it in local trivializations. Let $[x_0]\in X/G$. Since $q_X$ and $q_Y$ are double covers, there are open neighbourhoods $U\subset X/G$ of $[x_0]$ and $V\subset Y/G$ of $\bar f([x_0])$ such that $\bar f(U)\subset V$, together with homeomorphisms over the bases \begin{align*} \tau_X:q_X^{-1}(U)\to U\times G \end{align*} and \begin{align*} \tau_Y:q_Y^{-1}(V)\to V\times G. \end{align*} Under these trivializations, equivariance gives a locally constant function $a:U\to G$ such that \begin{align*} \tau_Y(f(z))=(\bar f(q_X(z)),a(q_X(z))h) \end{align*} whenever $\tau_X(z)=(q_X(z),h)$. Hence $\Phi$ is represented on $q_X^{-1}(U)$ by the map \begin{align*} U\times G\to U\times G \end{align*} given by $(u,h)\mapsto (u,a(u)h)$. Because $G$ is discrete and $a$ is locally constant, this map is a homeomorphism with inverse $(u,h)\mapsto (u,a(u)^{-1}h)$. These local inverses agree on overlaps, since they are inverses to the same globally defined map $\Phi$. Therefore $\Phi:X\to P$ is a homeomorphism over $X/G$, and $q_X$ is isomorphic to the pullback of $q_Y$ along $\bar f$ as a double cover.[/step]

[guided]The point of this step is to connect equivariance with characteristic classes. Characteristic classes live on the base spaces $X/G$ and $Y/G$, so we need an isomorphism of covers over $X/G$, not merely a bijection on each fibre. By hypothesis, $q_X:X\to X/G$ and $q_Y:Y\to Y/G$ are double covers. Define the pullback total space \begin{align*} P=\{([x],y)\in (X/G)\times Y:\bar f([x])=q_Y(y)\} \end{align*} and define $\pi:P\to X/G$ by $\pi([x],y)=[x]$. This is the pullback cover $\bar f^*q_Y\to X/G$. Now define \begin{align*} \Phi:X\to P \end{align*} by $\Phi(x)=([x],f(x))$. The defining condition for membership in $P$ is satisfied because $q_Y(f(x))=[f(x)]=\bar f([x])$. The map is continuous since its coordinate maps are $q_X$ and $f$, and $P$ carries the subspace topology from $(X/G)\times Y$. Also $\pi\circ\Phi=q_X$, so $\Phi$ lies over the identity map of $X/G$. Why is fibrewise bijectivity not enough? A continuous bijection can fail to be a homeomorphism unless additional topology is controlled. The double-cover hypothesis supplies that control through local trivializations. Fix $[x_0]\in X/G$. Since $q_X$ and $q_Y$ are double covers, choose open neighbourhoods $U\subset X/G$ of $[x_0]$ and $V\subset Y/G$ of $\bar f([x_0])$ with $\bar f(U)\subset V$, and choose homeomorphisms over the bases \begin{align*} \tau_X:q_X^{-1}(U)\to U\times G \end{align*} and \begin{align*} \tau_Y:q_Y^{-1}(V)\to V\times G. \end{align*} For $z\in q_X^{-1}(U)$, write $\tau_X(z)=(q_X(z),h)$ with $h\in G$. Equivariance of $f$ means that applying the nonidentity element of $G$ before $f$ is the same as applying it after $f$. Therefore, in these two-sheeted trivializations, $f$ must send the sheet labelled $h$ over $u$ to the sheet labelled $a(u)h$ over $\bar f(u)$ for a locally constant map $a:U\to G$. In symbols, \begin{align*} \tau_Y(f(z))=(\bar f(q_X(z)),a(q_X(z))h). \end{align*} Thus $\Phi$ is represented locally by \begin{align*} U\times G\to U\times G \end{align*} with $(u,h)\mapsto (u,a(u)h)$. Since $G=\mathbb Z/2$ is discrete and $a$ is locally constant, this local representative is a homeomorphism; its inverse is $(u,h)\mapsto (u,a(u)^{-1}h)$. These local homeomorphism statements cover all of $X/G$ and agree with the globally defined map $\Phi$, so $\Phi:X\to P$ is a homeomorphism over $X/G$. Therefore $q_X$ is isomorphic to the pullback of $q_Y$ along $\bar f$ as a double cover.[/guided]

[step:Pull back the first Stiefel-Whitney class] Let $w_X\in H^1(X/G;\mathbb F_2)$ denote the first Stiefel-Whitney class of the double cover $q_X:X\to X/G$, and let $w_Y\in H^1(Y/G;\mathbb F_2)$ denote the first Stiefel-Whitney class of the double cover $q_Y:Y\to Y/G$. The hypotheses of naturality for the first Stiefel-Whitney class are satisfied: $q_X$ and $q_Y$ are double covers by assumption, and the previous step proves that $q_X$ is isomorphic to the pullback double cover $\bar f^*q_Y$. Therefore naturality gives \begin{align*} \bar f^*(w_Y)=w_X \end{align*} in $H^1(X/G;\mathbb F_2)$. [/step]

[step:Compare nonzero powers under pullback] Let $k\in \mathbb N\cup\{0\}$ satisfy \begin{align*} w_X^k\neq 0 \end{align*} in $H^k(X/G;\mathbb F_2)$. Since cohomological pullback is a graded ring homomorphism with respect to the cup product, \begin{align*} \bar f^*(w_Y^k)=(\bar f^*w_Y)^k=w_X^k. \end{align*} Therefore $\bar f^*(w_Y^k)\neq 0$. If $w_Y^k=0$ in $H^k(Y/G;\mathbb F_2)$, then applying the homomorphism $\bar f^*$ would give $\bar f^*(w_Y^k)=0$, contradicting the displayed equality. Hence \begin{align*} w_Y^k\neq 0 \end{align*} in $H^k(Y/G;\mathbb F_2)$. [/step]

[step:Take the supremum over all nonzero powers] Define \begin{align*} A_X=\{k\in \mathbb N\cup\{0\}:w_X^k\neq 0\} \end{align*} and \begin{align*} A_Y=\{k\in \mathbb N\cup\{0\}:w_Y^k\neq 0\}. \end{align*} The previous step proves $A_X\subseteq A_Y$. Taking suprema in $\mathbb N\cup\{0,\infty\}$ gives \begin{align*} \operatorname{ind}(X)=\sup A_X\leq \sup A_Y=\operatorname{ind}(Y). \end{align*} This is the claimed monotonicity of the cohomological index. [/step]