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	syl5eq	⊢ ( 𝜑 → 𝐺 = ( 𝑂 /s ( ≃ph ‘ 𝐽 ) ) )