# Metamath Proof Explorer

## 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}↔\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}↔\left({F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge {F}\left(0\right)={Y}\wedge {F}\left(1\right)={Y}\right)\right)$