Theorem pi1val

Description: The definition of the fundamental group. (Contributed by Mario Carneiro, 11-Feb-2015) (Revised by Mario Carneiro, 10-Jul-2015)

	Ref	Expression
Hypotheses	pi1val.g	|- G = ( J pi1 Y )
	pi1val.1	|- ( ph -> J e. ( TopOn ` X ) )
	pi1val.2	|- ( ph -> Y e. X )
	pi1val.o	|- O = ( J Om1 Y )
Assertion	pi1val	|- ( ph -> G = ( O /s ( ~=ph ` J ) ) )

Proof

Step	Hyp	Ref	Expression
1		pi1val.g	|- G = ( J pi1 Y )
2		pi1val.1	|- ( ph -> J e. ( TopOn ` X ) )
3		pi1val.2	|- ( ph -> Y e. X )
4		pi1val.o	|- O = ( J Om1 Y )
5		df-pi1	|- pi1 = ( j e. Top , y e. U. j |-> ( ( j Om1 y ) /s ( ~=ph ` j ) ) )
6	5	a1i	|- ( ph -> pi1 = ( j e. Top , y e. U. j |-> ( ( j Om1 y ) /s ( ~=ph ` j ) ) ) )
7		simprl	|- ( ( ph /\ ( j = J /\ y = Y ) ) -> j = J )
8		simprr	|- ( ( ph /\ ( j = J /\ y = Y ) ) -> y = Y )
9	7 8	oveq12d	|- ( ( ph /\ ( j = J /\ y = Y ) ) -> ( j Om1 y ) = ( J Om1 Y ) )
10	9 4	eqtr4di	|- ( ( ph /\ ( j = J /\ y = Y ) ) -> ( j Om1 y ) = O )
11	7	fveq2d	|- ( ( ph /\ ( j = J /\ y = Y ) ) -> ( ~=ph ` j ) = ( ~=ph ` J ) )
12	10 11	oveq12d	|- ( ( ph /\ ( j = J /\ y = Y ) ) -> ( ( j Om1 y ) /s ( ~=ph ` j ) ) = ( O /s ( ~=ph ` J ) ) )
13		unieq	|- ( j = J -> U. j = U. J )
14	13	adantl	|- ( ( ph /\ j = J ) -> U. j = U. J )
15		toponuni	|- ( J e. ( TopOn ` X ) -> X = U. J )
16	2 15	syl	|- ( ph -> X = U. J )
17	16	adantr	|- ( ( ph /\ j = J ) -> X = U. J )
18	14 17	eqtr4d	|- ( ( ph /\ j = J ) -> U. j = X )
19		topontop	|- ( J e. ( TopOn ` X ) -> J e. Top )
20	2 19	syl	|- ( ph -> J e. Top )
21		ovexd	|- ( ph -> ( O /s ( ~=ph ` J ) ) e. _V )
22	6 12 18 20 3 21	ovmpodx	|- ( ph -> ( J pi1 Y ) = ( O /s ( ~=ph ` J ) ) )
23	1 22	syl5eq	|- ( ph -> G = ( O /s ( ~=ph ` J ) ) )