Metamath Proof Explorer


Theorem pi1bas2

Description: The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses pi1val.g 𝐺 = ( 𝐽 π1 𝑌 )
pi1val.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
pi1val.2 ( 𝜑𝑌𝑋 )
pi1bas2.b ( 𝜑𝐵 = ( Base ‘ 𝐺 ) )
Assertion pi1bas2 ( 𝜑𝐵 = ( 𝐵 / ( ≃ph𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 pi1val.g 𝐺 = ( 𝐽 π1 𝑌 )
2 pi1val.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 pi1val.2 ( 𝜑𝑌𝑋 )
4 pi1bas2.b ( 𝜑𝐵 = ( Base ‘ 𝐺 ) )
5 eqid ( 𝐽 Ω1 𝑌 ) = ( 𝐽 Ω1 𝑌 )
6 eqidd ( 𝜑 → ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
7 1 2 3 5 4 6 pi1buni ( 𝜑 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
8 1 2 3 5 4 7 pi1bas ( 𝜑𝐵 = ( 𝐵 / ( ≃ph𝐽 ) ) )