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 pi1 ( F ` 0 ) )
	pi1xfr.q	|- Q = ( J pi1 ( F ` 1 ) )
	pi1xfr.b	|- B = ( Base ` P )
	pi1xfr.g	|- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
	pi1xfr.j	|- ( ph -> J e. ( TopOn ` X ) )
	pi1xfr.f	|- ( ph -> F e. ( II Cn J ) )
	pi1xfr.i	|- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
Assertion	pi1xfrgim	|- ( ph -> G e. ( P GrpIso Q ) )

Proof

Step	Hyp	Ref	Expression
1		pi1xfr.p	|- P = ( J pi1 ( F ` 0 ) )
2		pi1xfr.q	|- Q = ( J pi1 ( F ` 1 ) )
3		pi1xfr.b	|- B = ( Base ` P )
4		pi1xfr.g	|- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
5		pi1xfr.j	|- ( ph -> J e. ( TopOn ` X ) )
6		pi1xfr.f	|- ( ph -> F e. ( II Cn J ) )
7		pi1xfr.i	|- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
8	1 2 3 4 5 6 7	pi1xfr	|- ( ph -> G e. ( P GrpHom Q ) )
9		eqid	|- ran ( y e. U. ( Base ` Q ) |-> <. [ y ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( y ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) = ran ( y e. U. ( Base ` Q ) |-> <. [ y ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( y ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )
10	1 2 3 4 5 6 7 9	pi1xfrcnv	|- ( ph -> ( `' G = ran ( y e. U. ( Base ` Q ) |-> <. [ y ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( y ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) /\ `' G e. ( Q GrpHom P ) ) )
11	10	simprd	|- ( ph -> `' G e. ( Q GrpHom P ) )
12		isgim2	|- ( G e. ( P GrpIso Q ) <-> ( G e. ( P GrpHom Q ) /\ `' G e. ( Q GrpHom P ) ) )
13	8 11 12	sylanbrc	|- ( ph -> G e. ( P GrpIso Q ) )