Theorem pi1eluni

Description: Elementhood in the base set of the loop space. (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	pi1eluni	$$⊢\phi \to \left(F\in \bigcup B\leftrightarrow \left(F\in \left(\mathrm{II}\mathrm{Cn}J\right)\wedge F\left(0\right)=Y\wedge F\left(1\right)=Y\right)\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	5 2 3 7	om1elbas	$$⊢\phi \to \left(F\in \bigcup B\leftrightarrow \left(F\in \left(\mathrm{II}\mathrm{Cn}J\right)\wedge F\left(0\right)=Y\wedge F\left(1\right)=Y\right)\right)$$