Theorem pi1xfrgim

Description: The mapping G between fundamental groups is an isomorphism. (Contributed by Mario Carneiro, 12-Feb-2015)

	Ref	Expression
Hypotheses	pi1xfr.p	$$⊢P=J{\pi }_{1}F\left(0\right)$$
	pi1xfr.q	$$⊢Q=J{\pi }_{1}F\left(1\right)$$
	pi1xfr.b	$$⊢B={\mathrm{Base}}_P$$
	pi1xfr.g	$$⊢G=\mathrm{ran}\left(g\in \bigcup B⟼⟨\left[g\right]{\simeq }_{\mathrm{ph}}\left(J\right),\left[\left(I{*}_{𝑝}\left(J\right)\left(g{*}_{𝑝}\left(J\right)F\right)\right)\right]{\simeq }_{\mathrm{ph}}\left(J\right)⟩\right)$$
	pi1xfr.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	pi1xfr.f	$$⊢\phi \to F\in \left(\mathrm{II}\mathrm{Cn}J\right)$$
	pi1xfr.i	$$⊢I=\left(x\in \left[0,1\right]⟼F\left(1-x\right)\right)$$
Assertion	pi1xfrgim	$$⊢\phi \to G\in \left(P\mathrm{GrpIso}Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		pi1xfr.p	$$⊢P=J{\pi }_{1}F\left(0\right)$$
2		pi1xfr.q	$$⊢Q=J{\pi }_{1}F\left(1\right)$$
3		pi1xfr.b	$$⊢B={\mathrm{Base}}_P$$
4		pi1xfr.g	$$⊢G=\mathrm{ran}\left(g\in \bigcup B⟼⟨\left[g\right]{\simeq }_{\mathrm{ph}}\left(J\right),\left[\left(I{*}_{𝑝}\left(J\right)\left(g{*}_{𝑝}\left(J\right)F\right)\right)\right]{\simeq }_{\mathrm{ph}}\left(J\right)⟩\right)$$
5		pi1xfr.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
6		pi1xfr.f	$$⊢\phi \to F\in \left(\mathrm{II}\mathrm{Cn}J\right)$$
7		pi1xfr.i	$$⊢I=\left(x\in \left[0,1\right]⟼F\left(1-x\right)\right)$$
8	1 2 3 4 5 6 7	pi1xfr	$$⊢\phi \to G\in \left(P\mathrm{GrpHom}Q\right)$$
9		eqid	$$⊢\mathrm{ran}\left(y\in \bigcup {\mathrm{Base}}_Q⟼⟨\left[y\right]{\simeq }_{\mathrm{ph}}\left(J\right),\left[\left(F{*}_{𝑝}\left(J\right)\left(y{*}_{𝑝}\left(J\right)I\right)\right)\right]{\simeq }_{\mathrm{ph}}\left(J\right)⟩\right)=\mathrm{ran}\left(y\in \bigcup {\mathrm{Base}}_Q⟼⟨\left[y\right]{\simeq }_{\mathrm{ph}}\left(J\right),\left[\left(F{*}_{𝑝}\left(J\right)\left(y{*}_{𝑝}\left(J\right)I\right)\right)\right]{\simeq }_{\mathrm{ph}}\left(J\right)⟩\right)$$
10	1 2 3 4 5 6 7 9	pi1xfrcnv	$$⊢\phi \to \left(G^{-1}=\mathrm{ran}\left(y\in \bigcup {\mathrm{Base}}_Q⟼⟨\left[y\right]{\simeq }_{\mathrm{ph}}\left(J\right),\left[\left(F{*}_{𝑝}\left(J\right)\left(y{*}_{𝑝}\left(J\right)I\right)\right)\right]{\simeq }_{\mathrm{ph}}\left(J\right)⟩\right)\wedge G^{-1}\in \left(Q\mathrm{GrpHom}P\right)\right)$$
11	10	simprd	$$⊢\phi \to G^{-1}\in \left(Q\mathrm{GrpHom}P\right)$$
12		isgim2	$$⊢G\in \left(P\mathrm{GrpIso}Q\right)\leftrightarrow \left(G\in \left(P\mathrm{GrpHom}Q\right)\wedge G^{-1}\in \left(Q\mathrm{GrpHom}P\right)\right)$$
13	8 11 12	sylanbrc	$$⊢\phi \to G\in \left(P\mathrm{GrpIso}Q\right)$$