Universal principal bundle of a subgroup $H \subseteq G$.

Question

This was claimed in the referenced link:

If $H \subseteq G$ is an admissible subgroup, i.e. $G \rightarrow G/H$ is a principal $H$ bundle.

Let $EG \rightarrow BG$ be a model universal principal bundle of $G$ (if exists).

Then $EG \times_H G\rightarrow EG/H$ is a universal principal bundle for $H$. i.e. $EG/H$ is classifying space for $H$.

This does not seem clear to me. How does the last line follow?

EDIT: It seems to me that it suffices to show

1. $EG \times_H G$ is a principal $H$-bundle.
2. It is weakly contractible, so we can apply theorem 7.4.

Reference: Page 17, paragraph before prop 8.3, notes by Stephen Mitchell

Answer 1

Since $EG$ is a free contractible $G$-space, it is a a free contractible $H$-space for any subgroup $H\leq G$. Hence the projection

$$p_H:EG\rightarrow EG/H$$

onto $H$-orbits will satisfy the properties for it to be the universal $H$-principal bundle as long as the local-triviality condition is met. This is Propositions 7.4, 7.5.

To see that it is indeed locally trivial we appeal to the single assumption. We use the bundle-isomorphisms

$$EG\cong EG\times_G G$$

and

$$EG/H\cong(EG\times_GG)/H\cong EG\times_G(G/H)$$

to see that $p_H$ is exactly the map

$$p_H:EG\times_GG\rightarrow EG\times_G(G/H).$$

Then local triviality follows from the work we did on a previous question you asked, since it is just the associated bundle to an admissible group quotient.

Edit: also see proposition 3.5.