Metamath Proof Explorer


Theorem pi1val

Description: The definition of the fundamental group. (Contributed by Mario Carneiro, 11-Feb-2015) (Revised by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses pi1val.g 𝐺 = ( 𝐽 π1 𝑌 )
pi1val.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
pi1val.2 ( 𝜑𝑌𝑋 )
pi1val.o 𝑂 = ( 𝐽 Ω1 𝑌 )
Assertion pi1val ( 𝜑𝐺 = ( 𝑂 /s ( ≃ph𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 pi1val.g 𝐺 = ( 𝐽 π1 𝑌 )
2 pi1val.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 pi1val.2 ( 𝜑𝑌𝑋 )
4 pi1val.o 𝑂 = ( 𝐽 Ω1 𝑌 )
5 df-pi1 π1 = ( 𝑗 ∈ Top , 𝑦 𝑗 ↦ ( ( 𝑗 Ω1 𝑦 ) /s ( ≃ph𝑗 ) ) )
6 5 a1i ( 𝜑 → π1 = ( 𝑗 ∈ Top , 𝑦 𝑗 ↦ ( ( 𝑗 Ω1 𝑦 ) /s ( ≃ph𝑗 ) ) ) )
7 simprl ( ( 𝜑 ∧ ( 𝑗 = 𝐽𝑦 = 𝑌 ) ) → 𝑗 = 𝐽 )
8 simprr ( ( 𝜑 ∧ ( 𝑗 = 𝐽𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
9 7 8 oveq12d ( ( 𝜑 ∧ ( 𝑗 = 𝐽𝑦 = 𝑌 ) ) → ( 𝑗 Ω1 𝑦 ) = ( 𝐽 Ω1 𝑌 ) )
10 9 4 eqtr4di ( ( 𝜑 ∧ ( 𝑗 = 𝐽𝑦 = 𝑌 ) ) → ( 𝑗 Ω1 𝑦 ) = 𝑂 )
11 7 fveq2d ( ( 𝜑 ∧ ( 𝑗 = 𝐽𝑦 = 𝑌 ) ) → ( ≃ph𝑗 ) = ( ≃ph𝐽 ) )
12 10 11 oveq12d ( ( 𝜑 ∧ ( 𝑗 = 𝐽𝑦 = 𝑌 ) ) → ( ( 𝑗 Ω1 𝑦 ) /s ( ≃ph𝑗 ) ) = ( 𝑂 /s ( ≃ph𝐽 ) ) )
13 unieq ( 𝑗 = 𝐽 𝑗 = 𝐽 )
14 13 adantl ( ( 𝜑𝑗 = 𝐽 ) → 𝑗 = 𝐽 )
15 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
16 2 15 syl ( 𝜑𝑋 = 𝐽 )
17 16 adantr ( ( 𝜑𝑗 = 𝐽 ) → 𝑋 = 𝐽 )
18 14 17 eqtr4d ( ( 𝜑𝑗 = 𝐽 ) → 𝑗 = 𝑋 )
19 topontop ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
20 2 19 syl ( 𝜑𝐽 ∈ Top )
21 ovexd ( 𝜑 → ( 𝑂 /s ( ≃ph𝐽 ) ) ∈ V )
22 6 12 18 20 3 21 ovmpodx ( 𝜑 → ( 𝐽 π1 𝑌 ) = ( 𝑂 /s ( ≃ph𝐽 ) ) )
23 1 22 eqtrid ( 𝜑𝐺 = ( 𝑂 /s ( ≃ph𝐽 ) ) )