Theorem pi1xfrgim

Description: The mapping G between fundamental groups is an isomorphism. (Contributed by Mario Carneiro, 12-Feb-2015)

	Ref	Expression
Hypotheses	pi1xfr.p	⊢ 𝑃 = ( 𝐽 π1 ( 𝐹 ‘ 0 ) )
	pi1xfr.q	⊢ 𝑄 = ( 𝐽 π1 ( 𝐹 ‘ 1 ) )
	pi1xfr.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	pi1xfr.g	⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
	pi1xfr.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	pi1xfr.f	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
	pi1xfr.i	⊢ 𝐼 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
Assertion	pi1xfrgim	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 GrpIso 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		pi1xfr.p	⊢ 𝑃 = ( 𝐽 π1 ( 𝐹 ‘ 0 ) )
2		pi1xfr.q	⊢ 𝑄 = ( 𝐽 π1 ( 𝐹 ‘ 1 ) )
3		pi1xfr.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		pi1xfr.g	⊢ 𝐺 = ran ( 𝑔 ∈ ∪ 𝐵 ↦ ⟨ [ 𝑔 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐼 ( *𝑝 ‘ 𝐽 ) ( 𝑔 ( *𝑝 ‘ 𝐽 ) 𝐹 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
5		pi1xfr.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6		pi1xfr.f	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
7		pi1xfr.i	⊢ 𝐼 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 − 𝑥 ) ) )
8	1 2 3 4 5 6 7	pi1xfr	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 GrpHom 𝑄 ) )
9		eqid	⊢ ran ( 𝑦 ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ 𝑦 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) = ran ( 𝑦 ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ 𝑦 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ )
10	1 2 3 4 5 6 7 9	pi1xfrcnv	⊢ ( 𝜑 → ( ◡ 𝐺 = ran ( 𝑦 ∈ ∪ ( Base ‘ 𝑄 ) ↦ ⟨ [ 𝑦 ] ( ≃ph ‘ 𝐽 ) , [ ( 𝐹 ( *𝑝 ‘ 𝐽 ) ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝐼 ) ) ] ( ≃ph ‘ 𝐽 ) ⟩ ) ∧ ◡ 𝐺 ∈ ( 𝑄 GrpHom 𝑃 ) ) )
11	10	simprd	⊢ ( 𝜑 → ◡ 𝐺 ∈ ( 𝑄 GrpHom 𝑃 ) )
12		isgim2	⊢ ( 𝐺 ∈ ( 𝑃 GrpIso 𝑄 ) ↔ ( 𝐺 ∈ ( 𝑃 GrpHom 𝑄 ) ∧ ◡ 𝐺 ∈ ( 𝑄 GrpHom 𝑃 ) ) )
13	8 11 12	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 GrpIso 𝑄 ) )