Metamath Proof Explorer


Theorem pi1bas

Description: The base set of the fundamental group of a topological space at a given base point. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses pi1val.g 𝐺 = ( 𝐽 π1 𝑌 )
pi1val.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
pi1val.2 ( 𝜑𝑌𝑋 )
pi1val.o 𝑂 = ( 𝐽 Ω1 𝑌 )
pi1bas.b ( 𝜑𝐵 = ( Base ‘ 𝐺 ) )
pi1bas.k ( 𝜑𝐾 = ( Base ‘ 𝑂 ) )
Assertion pi1bas ( 𝜑𝐵 = ( 𝐾 / ( ≃ph𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 pi1val.g 𝐺 = ( 𝐽 π1 𝑌 )
2 pi1val.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 pi1val.2 ( 𝜑𝑌𝑋 )
4 pi1val.o 𝑂 = ( 𝐽 Ω1 𝑌 )
5 pi1bas.b ( 𝜑𝐵 = ( Base ‘ 𝐺 ) )
6 pi1bas.k ( 𝜑𝐾 = ( Base ‘ 𝑂 ) )
7 1 2 3 4 pi1val ( 𝜑𝐺 = ( 𝑂 /s ( ≃ph𝐽 ) ) )
8 eqidd ( 𝜑 → ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 ) )
9 fvexd ( 𝜑 → ( ≃ph𝐽 ) ∈ V )
10 4 ovexi 𝑂 ∈ V
11 10 a1i ( 𝜑𝑂 ∈ V )
12 7 8 9 11 qusbas ( 𝜑 → ( ( Base ‘ 𝑂 ) / ( ≃ph𝐽 ) ) = ( Base ‘ 𝐺 ) )
13 qseq1 ( 𝐾 = ( Base ‘ 𝑂 ) → ( 𝐾 / ( ≃ph𝐽 ) ) = ( ( Base ‘ 𝑂 ) / ( ≃ph𝐽 ) ) )
14 6 13 syl ( 𝜑 → ( 𝐾 / ( ≃ph𝐽 ) ) = ( ( Base ‘ 𝑂 ) / ( ≃ph𝐽 ) ) )
15 12 14 5 3eqtr4rd ( 𝜑𝐵 = ( 𝐾 / ( ≃ph𝐽 ) ) )