Theorem pi1bas2

Description: The base set of the fundamental group, written self-referentially. (Contributed 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$$
	pi1bas2.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
Assertion	pi1bas2	$$⊢\phi \to B=\bigcup B/{\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		pi1bas2.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
5		eqid	$$⊢J{\Omega }_{1}Y=J{\Omega }_{1}Y$$
6		eqidd	$$⊢\phi \to {\mathrm{Base}}_{\left(J{\Omega }_{1}Y\right)}={\mathrm{Base}}_{\left(J{\Omega }_{1}Y\right)}$$
7	1 2 3 5 4 6	pi1buni	$$⊢\phi \to \bigcup B={\mathrm{Base}}_{\left(J{\Omega }_{1}Y\right)}$$
8	1 2 3 5 4 7	pi1bas	$$⊢\phi \to B=\bigcup B/{\simeq }_{\mathrm{ph}}\left(J\right)$$