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	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
	pi1id.3	⊢ 0 = ( ( 0 [,] 1 ) × { 𝑌 } )
Assertion	pi1id	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ) → [ 0 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		pi1grp.2	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
2		pi1id.3	⊢ 0 = ( ( 0 [,] 1 ) × { 𝑌 } )
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4		simpl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5		simpr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ) → 𝑌 ∈ 𝑋 )
6	1 3 4 5 2	pi1grplem	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ) → ( 𝐺 ∈ Grp ∧ [ 0 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ 𝐺 ) ) )
7	6	simprd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ) → [ 0 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ 𝐺 ) )