# Metamath Proof Explorer

## Theorem elpi1i

Description: The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses elpi1.g ${⊢}{G}={J}{\pi }_{1}{Y}$
elpi1.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
elpi1.1 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
elpi1.2 ${⊢}{\phi }\to {Y}\in {X}$
elpi1i.3 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
elpi1i.4 ${⊢}{\phi }\to {F}\left(0\right)={Y}$
elpi1i.5 ${⊢}{\phi }\to {F}\left(1\right)={Y}$
Assertion elpi1i ${⊢}{\phi }\to \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\in {B}$

### Proof

Step Hyp Ref Expression
1 elpi1.g ${⊢}{G}={J}{\pi }_{1}{Y}$
2 elpi1.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
3 elpi1.1 ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
4 elpi1.2 ${⊢}{\phi }\to {Y}\in {X}$
5 elpi1i.3 ${⊢}{\phi }\to {F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
6 elpi1i.4 ${⊢}{\phi }\to {F}\left(0\right)={Y}$
7 elpi1i.5 ${⊢}{\phi }\to {F}\left(1\right)={Y}$
8 eceq1 ${⊢}{f}={F}\to \left[{f}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)$
9 8 eqcomd ${⊢}{f}={F}\to \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{f}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)$
10 9 biantrud ${⊢}{f}={F}\to \left(\left({f}\left(0\right)={Y}\wedge {f}\left(1\right)={Y}\right)↔\left(\left({f}\left(0\right)={Y}\wedge {f}\left(1\right)={Y}\right)\wedge \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{f}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\right)\right)$
11 fveq1 ${⊢}{f}={F}\to {f}\left(0\right)={F}\left(0\right)$
12 11 eqeq1d ${⊢}{f}={F}\to \left({f}\left(0\right)={Y}↔{F}\left(0\right)={Y}\right)$
13 fveq1 ${⊢}{f}={F}\to {f}\left(1\right)={F}\left(1\right)$
14 13 eqeq1d ${⊢}{f}={F}\to \left({f}\left(1\right)={Y}↔{F}\left(1\right)={Y}\right)$
15 12 14 anbi12d ${⊢}{f}={F}\to \left(\left({f}\left(0\right)={Y}\wedge {f}\left(1\right)={Y}\right)↔\left({F}\left(0\right)={Y}\wedge {F}\left(1\right)={Y}\right)\right)$
16 10 15 bitr3d ${⊢}{f}={F}\to \left(\left(\left({f}\left(0\right)={Y}\wedge {f}\left(1\right)={Y}\right)\wedge \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{f}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\right)↔\left({F}\left(0\right)={Y}\wedge {F}\left(1\right)={Y}\right)\right)$
17 16 rspcev ${⊢}\left({F}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({F}\left(0\right)={Y}\wedge {F}\left(1\right)={Y}\right)\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}\left(0\right)={Y}\wedge {f}\left(1\right)={Y}\right)\wedge \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{f}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\right)$
18 5 6 7 17 syl12anc ${⊢}{\phi }\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}\left(0\right)={Y}\wedge {f}\left(1\right)={Y}\right)\wedge \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{f}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\right)$
19 1 2 3 4 elpi1 ${⊢}{\phi }\to \left(\left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\in {B}↔\exists {f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}\left(\left({f}\left(0\right)={Y}\wedge {f}\left(1\right)={Y}\right)\wedge \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)=\left[{f}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\right)\right)$
20 18 19 mpbird ${⊢}{\phi }\to \left[{F}\right]{\simeq }_{\mathrm{ph}}\left({J}\right)\in {B}$