Theorem pi1buni

Description: Another way to write the loop space base in terms of the base 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$$
	pi1val.o	$$⊢O=J{\Omega }_{1}Y$$
	pi1bas.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
	pi1bas.k	$$⊢\phi \to K={\mathrm{Base}}_O$$
Assertion	pi1buni	$$⊢\phi \to \bigcup B=K$$

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 5 6	pi1bas	$$⊢\phi \to B=K/{\simeq }_{\mathrm{ph}}\left(J\right)$$
8	1 2 3 4 5 6	pi1blem	$$⊢\phi \to \left({\simeq }_{\mathrm{ph}}\left(J\right)\left[K\right]\subseteq K\wedge K\subseteq \mathrm{II}\mathrm{Cn}J\right)$$
9	8	simpld	$$⊢\phi \to {\simeq }_{\mathrm{ph}}\left(J\right)\left[K\right]\subseteq K$$
10		qsinxp	$$⊢{\simeq }_{\mathrm{ph}}\left(J\right)\left[K\right]\subseteq K\to K/{\simeq }_{\mathrm{ph}}\left(J\right)=K/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(K\times K\right)\right)$$
11	9 10	syl	$$⊢\phi \to K/{\simeq }_{\mathrm{ph}}\left(J\right)=K/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(K\times K\right)\right)$$
12	7 11	eqtrd	$$⊢\phi \to B=K/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(K\times K\right)\right)$$
13	12	unieqd	$$⊢\phi \to \bigcup B=\bigcup \left(K/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(K\times K\right)\right)\right)$$
14		phtpcer	$$⊢{\simeq }_{\mathrm{ph}}\left(J\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}J\right)$$
15	14	a1i	$$⊢\phi \to {\simeq }_{\mathrm{ph}}\left(J\right)\mathrm{Er}\left(\mathrm{II}\mathrm{Cn}J\right)$$
16	8	simprd	$$⊢\phi \to K\subseteq \mathrm{II}\mathrm{Cn}J$$
17	15 16	erinxp	$$⊢\phi \to \left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(K\times K\right)\right)\mathrm{Er}K$$
18		fvex	$$⊢{\simeq }_{\mathrm{ph}}\left(J\right)\in \mathrm{V}$$
19	18	inex1	$$⊢{\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(K\times K\right)\in \mathrm{V}$$
20	19	a1i	$$⊢\phi \to {\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(K\times K\right)\in \mathrm{V}$$
21	17 20	uniqs2	$$⊢\phi \to \bigcup \left(K/\left({\simeq }_{\mathrm{ph}}\left(J\right)\cap \left(K\times K\right)\right)\right)=K$$
22	13 21	eqtrd	$$⊢\phi \to \bigcup B=K$$