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	$$⊢G=J{\pi }_{1}Y$$
	pi1val.1	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	pi1val.2	$$⊢\phi \to Y\in X$$
	pi1val.o	$$⊢O=J{\Omega }_{1}Y$$
	pi1bas.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
	pi1bas.k	$$⊢\phi \to K={\mathrm{Base}}_O$$
Assertion	pi1bas	$$⊢\phi \to B=K/{\simeq }_{\mathrm{ph}}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		pi1val.g	$$⊢G=J{\pi }_{1}Y$$
2		pi1val.1	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
3		pi1val.2	$$⊢\phi \to Y\in X$$
4		pi1val.o	$$⊢O=J{\Omega }_{1}Y$$
5		pi1bas.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
6		pi1bas.k	$$⊢\phi \to K={\mathrm{Base}}_O$$
7	1 2 3 4	pi1val	$$⊢\phi \to G=O{/}_{𝑠}{\simeq }_{\mathrm{ph}}\left(J\right)$$
8		eqidd	$$⊢\phi \to {\mathrm{Base}}_O={\mathrm{Base}}_O$$
9		fvexd	$$⊢\phi \to {\simeq }_{\mathrm{ph}}\left(J\right)\in \mathrm{V}$$
10	4	ovexi	$$⊢O\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to O\in \mathrm{V}$$
12	7 8 9 11	qusbas	$$⊢\phi \to {\mathrm{Base}}_O/{\simeq }_{\mathrm{ph}}\left(J\right)={\mathrm{Base}}_G$$
13		qseq1	$$⊢K={\mathrm{Base}}_O\to K/{\simeq }_{\mathrm{ph}}\left(J\right)={\mathrm{Base}}_O/{\simeq }_{\mathrm{ph}}\left(J\right)$$
14	6 13	syl	$$⊢\phi \to K/{\simeq }_{\mathrm{ph}}\left(J\right)={\mathrm{Base}}_O/{\simeq }_{\mathrm{ph}}\left(J\right)$$
15	12 14 5	3eqtr4rd	$$⊢\phi \to B=K/{\simeq }_{\mathrm{ph}}\left(J\right)$$