Theorem pi1bas3

Description: The base set of the fundamental group. (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$$
	pi1bas3.r	$$⊢R={\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)$$
Assertion	pi1bas3	$$⊢\phi \to B=\bigcup B/R$$

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		pi1bas3.r	$$⊢R={\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)$$
6	1 2 3 4	pi1bas2	$$⊢\phi \to B=\bigcup B/{\simeq }_{\mathrm{ph}}\left(J\right)$$
7		eqid	$$⊢J{\Omega }_{1}Y=J{\Omega }_{1}Y$$
8		eqidd	$$⊢\phi \to {\mathrm{Base}}_{\left(J{\Omega }_{1}Y\right)}={\mathrm{Base}}_{\left(J{\Omega }_{1}Y\right)}$$
9	1 2 3 7 4 8	pi1buni	$$⊢\phi \to \bigcup B={\mathrm{Base}}_{\left(J{\Omega }_{1}Y\right)}$$
10	1 2 3 7 4 9	pi1blem	$$⊢\phi \to \left({\simeq }_{\mathrm{ph}}\left(J\right)\left[\bigcup B\right]\subseteq \bigcup B\wedge \bigcup B\subseteq \mathrm{II}\mathrm{Cn}J\right)$$
11	10	simpld	$$⊢\phi \to {\simeq }_{\mathrm{ph}}\left(J\right)\left[\bigcup B\right]\subseteq \bigcup B$$
12		qsinxp	$$⊢{\simeq }_{\mathrm{ph}}\left(J\right)\left[\bigcup B\right]\subseteq \bigcup B\to \bigcup B/{\simeq }_{\mathrm{ph}}\left(J\right)=\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)$$
13	11 12	syl	$$⊢\phi \to \bigcup B/{\simeq }_{\mathrm{ph}}\left(J\right)=\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)$$
14	6 13	eqtrd	$$⊢\phi \to B=\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)$$
15		qseq2	$$⊢R={\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\to \bigcup B/R=\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)$$
16	5 15	ax-mp	$$⊢\bigcup B/R=\bigcup B/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(\bigcup B\times \bigcup B\right)\right)$$
17	14 16	syl6eqr	$$⊢\phi \to B=\bigcup B/R$$