Metamath Proof Explorer


Theorem pi1bas3

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

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

Proof

Step Hyp Ref Expression
1 pi1val.g 𝐺 = ( 𝐽 π1 𝑌 )
2 pi1val.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 pi1val.2 ( 𝜑𝑌𝑋 )
4 pi1bas2.b ( 𝜑𝐵 = ( Base ‘ 𝐺 ) )
5 pi1bas3.r 𝑅 = ( ( ≃ph𝐽 ) ∩ ( 𝐵 × 𝐵 ) )
6 1 2 3 4 pi1bas2 ( 𝜑𝐵 = ( 𝐵 / ( ≃ph𝐽 ) ) )
7 eqid ( 𝐽 Ω1 𝑌 ) = ( 𝐽 Ω1 𝑌 )
8 eqidd ( 𝜑 → ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
9 1 2 3 7 4 8 pi1buni ( 𝜑 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
10 1 2 3 7 4 9 pi1blem ( 𝜑 → ( ( ( ≃ph𝐽 ) “ 𝐵 ) ⊆ 𝐵 𝐵 ⊆ ( II Cn 𝐽 ) ) )
11 10 simpld ( 𝜑 → ( ( ≃ph𝐽 ) “ 𝐵 ) ⊆ 𝐵 )
12 qsinxp ( ( ( ≃ph𝐽 ) “ 𝐵 ) ⊆ 𝐵 → ( 𝐵 / ( ≃ph𝐽 ) ) = ( 𝐵 / ( ( ≃ph𝐽 ) ∩ ( 𝐵 × 𝐵 ) ) ) )
13 11 12 syl ( 𝜑 → ( 𝐵 / ( ≃ph𝐽 ) ) = ( 𝐵 / ( ( ≃ph𝐽 ) ∩ ( 𝐵 × 𝐵 ) ) ) )
14 6 13 eqtrd ( 𝜑𝐵 = ( 𝐵 / ( ( ≃ph𝐽 ) ∩ ( 𝐵 × 𝐵 ) ) ) )
15 qseq2 ( 𝑅 = ( ( ≃ph𝐽 ) ∩ ( 𝐵 × 𝐵 ) ) → ( 𝐵 / 𝑅 ) = ( 𝐵 / ( ( ≃ph𝐽 ) ∩ ( 𝐵 × 𝐵 ) ) ) )
16 5 15 ax-mp ( 𝐵 / 𝑅 ) = ( 𝐵 / ( ( ≃ph𝐽 ) ∩ ( 𝐵 × 𝐵 ) ) )
17 14 16 eqtr4di ( 𝜑𝐵 = ( 𝐵 / 𝑅 ) )