Theorem pi1id

Description: The identity element of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015) (Revised by Mario Carneiro, 10-Aug-2015)

	Ref	Expression
Hypotheses	pi1grp.2	$$⊢G=J{\pi }_{1}Y$$
	pi1id.3	$$⊢\underset{\dot{}}{0}=\left[0,1\right]\times \left\{Y\right\}$$
Assertion	pi1id	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge Y\in X\right)\to \left[\underset{\dot{}}{0}\right]{\simeq }_{\mathrm{ph}}\left(J\right)=0_G$$

Proof

Step	Hyp	Ref	Expression
1		pi1grp.2	$$⊢G=J{\pi }_{1}Y$$
2		pi1id.3	$$⊢\underset{\dot{}}{0}=\left[0,1\right]\times \left\{Y\right\}$$
3		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
4		simpl	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge Y\in X\right)\to J\in \mathrm{TopOn}\left(X\right)$$
5		simpr	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge Y\in X\right)\to Y\in X$$
6	1 3 4 5 2	pi1grplem	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge Y\in X\right)\to \left(G\in \mathrm{Grp}\wedge \left[\underset{\dot{}}{0}\right]{\simeq }_{\mathrm{ph}}\left(J\right)=0_G\right)$$
7	6	simprd	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge Y\in X\right)\to \left[\underset{\dot{}}{0}\right]{\simeq }_{\mathrm{ph}}\left(J\right)=0_G$$