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 pi1 Y )
elpi1.b 
|- B = ( Base ` G )
elpi1.1 
|- ( ph -> J e. ( TopOn ` X ) )
elpi1.2 
|- ( ph -> Y e. X )
elpi1i.3 
|- ( ph -> F e. ( II Cn J ) )
elpi1i.4 
|- ( ph -> ( F ` 0 ) = Y )
elpi1i.5 
|- ( ph -> ( F ` 1 ) = Y )
Assertion elpi1i 
|- ( ph -> [ F ] ( ~=ph ` J ) e. B )

Proof

Step Hyp Ref Expression
1 elpi1.g 
 |-  G = ( J pi1 Y )
2 elpi1.b 
 |-  B = ( Base ` G )
3 elpi1.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 elpi1.2 
 |-  ( ph -> Y e. X )
5 elpi1i.3 
 |-  ( ph -> F e. ( II Cn J ) )
6 elpi1i.4 
 |-  ( ph -> ( F ` 0 ) = Y )
7 elpi1i.5 
 |-  ( ph -> ( F ` 1 ) = Y )
8 eceq1 
 |-  ( f = F -> [ f ] ( ~=ph ` J ) = [ F ] ( ~=ph ` J ) )
9 8 eqcomd 
 |-  ( f = F -> [ F ] ( ~=ph ` J ) = [ f ] ( ~=ph ` J ) )
10 9 biantrud 
 |-  ( f = F -> ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) <-> ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ [ F ] ( ~=ph ` J ) = [ f ] ( ~=ph ` J ) ) ) )
11 fveq1 
 |-  ( f = F -> ( f ` 0 ) = ( F ` 0 ) )
12 11 eqeq1d 
 |-  ( f = F -> ( ( f ` 0 ) = Y <-> ( F ` 0 ) = Y ) )
13 fveq1 
 |-  ( f = F -> ( f ` 1 ) = ( F ` 1 ) )
14 13 eqeq1d 
 |-  ( f = F -> ( ( f ` 1 ) = Y <-> ( F ` 1 ) = Y ) )
15 12 14 anbi12d 
 |-  ( f = F -> ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) <-> ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )
16 10 15 bitr3d 
 |-  ( f = F -> ( ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ [ F ] ( ~=ph ` J ) = [ f ] ( ~=ph ` J ) ) <-> ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) )
17 16 rspcev 
 |-  ( ( F e. ( II Cn J ) /\ ( ( F ` 0 ) = Y /\ ( F ` 1 ) = Y ) ) -> E. f e. ( II Cn J ) ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ [ F ] ( ~=ph ` J ) = [ f ] ( ~=ph ` J ) ) )
18 5 6 7 17 syl12anc 
 |-  ( ph -> E. f e. ( II Cn J ) ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ [ F ] ( ~=ph ` J ) = [ f ] ( ~=ph ` J ) ) )
19 1 2 3 4 elpi1 
 |-  ( ph -> ( [ F ] ( ~=ph ` J ) e. B <-> E. f e. ( II Cn J ) ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ [ F ] ( ~=ph ` J ) = [ f ] ( ~=ph ` J ) ) ) )
20 18 19 mpbird 
 |-  ( ph -> [ F ] ( ~=ph ` J ) e. B )