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 π 1 Y
elpi1.b B = Base G
elpi1.1 φ J TopOn X
elpi1.2 φ Y X
Assertion elpi1 φ F B f II Cn J f 0 = Y f 1 = Y F = f ph J

Proof

Step Hyp Ref Expression
1 elpi1.g G = J π 1 Y
2 elpi1.b B = Base G
3 elpi1.1 φ J TopOn X
4 elpi1.2 φ Y X
5 2 a1i φ B = Base G
6 1 3 4 5 pi1bas2 φ B = B / ph J
7 6 eleq2d φ F B F B / ph J
8 elex F B / ph J F V
9 id F = f ph J F = f ph J
10 fvex ph J V
11 ecexg ph J V f ph J V
12 10 11 ax-mp f ph J V
13 9 12 eqeltrdi F = f ph J F V
14 13 rexlimivw f B F = f ph J F V
15 elqsg F V F B / ph J f B F = f ph J
16 8 14 15 pm5.21nii F B / ph J f B F = f ph J
17 1 3 4 5 pi1eluni φ f B f II Cn J f 0 = Y f 1 = Y
18 3anass f II Cn J f 0 = Y f 1 = Y f II Cn J f 0 = Y f 1 = Y
19 17 18 bitrdi φ f B f II Cn J f 0 = Y f 1 = Y
20 19 anbi1d φ f B F = f ph J f II Cn J f 0 = Y f 1 = Y F = f ph J
21 anass f II Cn J f 0 = Y f 1 = Y F = f ph J f II Cn J f 0 = Y f 1 = Y F = f ph J
22 20 21 bitrdi φ f B F = f ph J f II Cn J f 0 = Y f 1 = Y F = f ph J
23 22 rexbidv2 φ f B F = f ph J f II Cn J f 0 = Y f 1 = Y F = f ph J
24 16 23 syl5bb φ F B / ph J f II Cn J f 0 = Y f 1 = Y F = f ph J
25 7 24 bitrd φ F B f II Cn J f 0 = Y f 1 = Y F = f ph J