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 pi1 Y )
	pi1id.3	|- .0. = ( ( 0 [,] 1 ) X. { Y } )
Assertion	pi1id	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> [ .0. ] ( ~=ph ` J ) = ( 0g ` G ) )

Proof

Step	Hyp	Ref	Expression
1		pi1grp.2	|- G = ( J pi1 Y )
2		pi1id.3	|- .0. = ( ( 0 [,] 1 ) X. { Y } )
3		eqid	|- ( Base ` G ) = ( Base ` G )
4		simpl	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> J e. ( TopOn ` X ) )
5		simpr	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> Y e. X )
6	1 3 4 5 2	pi1grplem	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( G e. Grp /\ [ .0. ] ( ~=ph ` J ) = ( 0g ` G ) ) )
7	6	simprd	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> [ .0. ] ( ~=ph ` J ) = ( 0g ` G ) )