Metamath Proof Explorer

Theorem elpi1

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 )
Assertion elpi1 
|- ( ph -> ( F e. B <-> E. f e. ( II Cn J ) ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ F = [ f ] ( ~=ph ` J ) ) ) )

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 2 a1i 
 |-  ( ph -> B = ( Base ` G ) )
6 1 3 4 5 pi1bas2 
 |-  ( ph -> B = ( U. B /. ( ~=ph ` J ) ) )
7 6 eleq2d 
 |-  ( ph -> ( F e. B <-> F e. ( U. B /. ( ~=ph ` J ) ) ) )
8 elex 
 |-  ( F e. ( U. B /. ( ~=ph ` J ) ) -> F e. _V )
9 id 
 |-  ( F = [ f ] ( ~=ph ` J ) -> F = [ f ] ( ~=ph ` J ) )
10 fvex 
 |-  ( ~=ph ` J ) e. _V
11 ecexg 
 |-  ( ( ~=ph ` J ) e. _V -> [ f ] ( ~=ph ` J ) e. _V )
12 10 11 ax-mp 
 |-  [ f ] ( ~=ph ` J ) e. _V
13 9 12 eqeltrdi 
 |-  ( F = [ f ] ( ~=ph ` J ) -> F e. _V )
14 13 rexlimivw 
 |-  ( E. f e. U. B F = [ f ] ( ~=ph ` J ) -> F e. _V )
15 elqsg 
 |-  ( F e. _V -> ( F e. ( U. B /. ( ~=ph ` J ) ) <-> E. f e. U. B F = [ f ] ( ~=ph ` J ) ) )
16 8 14 15 pm5.21nii 
 |-  ( F e. ( U. B /. ( ~=ph ` J ) ) <-> E. f e. U. B F = [ f ] ( ~=ph ` J ) )
17 1 3 4 5 pi1eluni 
 |-  ( ph -> ( f e. U. B <-> ( f e. ( II Cn J ) /\ ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) ) )
18 3anass 
 |-  ( ( f e. ( II Cn J ) /\ ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) <-> ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) ) )
19 17 18 bitrdi 
 |-  ( ph -> ( f e. U. B <-> ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) ) ) )
20 19 anbi1d 
 |-  ( ph -> ( ( f e. U. B /\ F = [ f ] ( ~=ph ` J ) ) <-> ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) ) /\ F = [ f ] ( ~=ph ` J ) ) ) )
21 anass 
 |-  ( ( ( f e. ( II Cn J ) /\ ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) ) /\ F = [ f ] ( ~=ph ` J ) ) <-> ( f e. ( II Cn J ) /\ ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ F = [ f ] ( ~=ph ` J ) ) ) )
22 20 21 bitrdi 
 |-  ( ph -> ( ( f e. U. B /\ F = [ f ] ( ~=ph ` J ) ) <-> ( f e. ( II Cn J ) /\ ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ F = [ f ] ( ~=ph ` J ) ) ) ) )
23 22 rexbidv2 
 |-  ( ph -> ( E. f e. U. B F = [ f ] ( ~=ph ` J ) <-> E. f e. ( II Cn J ) ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ F = [ f ] ( ~=ph ` J ) ) ) )
24 16 23 syl5bb 
 |-  ( ph -> ( F e. ( U. B /. ( ~=ph ` J ) ) <-> E. f e. ( II Cn J ) ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ F = [ f ] ( ~=ph ` J ) ) ) )
25 7 24 bitrd 
 |-  ( ph -> ( F e. B <-> E. f e. ( II Cn J ) ( ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) /\ F = [ f ] ( ~=ph ` J ) ) ) )