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 ‘ 𝐽 ) ) )