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 𝐺 = ( 𝐽 π1 𝑌 )
elpi1.b 𝐵 = ( Base ‘ 𝐺 )
elpi1.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
elpi1.2 ( 𝜑𝑌𝑋 )
Assertion elpi1 ( 𝜑 → ( 𝐹𝐵 ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 elpi1.g 𝐺 = ( 𝐽 π1 𝑌 )
2 elpi1.b 𝐵 = ( Base ‘ 𝐺 )
3 elpi1.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 elpi1.2 ( 𝜑𝑌𝑋 )
5 2 a1i ( 𝜑𝐵 = ( Base ‘ 𝐺 ) )
6 1 3 4 5 pi1bas2 ( 𝜑𝐵 = ( 𝐵 / ( ≃ph𝐽 ) ) )
7 6 eleq2d ( 𝜑 → ( 𝐹𝐵𝐹 ∈ ( 𝐵 / ( ≃ph𝐽 ) ) ) )
8 elex ( 𝐹 ∈ ( 𝐵 / ( ≃ph𝐽 ) ) → 𝐹 ∈ V )
9 id ( 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) → 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) )
10 fvex ( ≃ph𝐽 ) ∈ V
11 ecexg ( ( ≃ph𝐽 ) ∈ V → [ 𝑓 ] ( ≃ph𝐽 ) ∈ V )
12 10 11 ax-mp [ 𝑓 ] ( ≃ph𝐽 ) ∈ V
13 9 12 eqeltrdi ( 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) → 𝐹 ∈ V )
14 13 rexlimivw ( ∃ 𝑓 𝐵 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) → 𝐹 ∈ V )
15 elqsg ( 𝐹 ∈ V → ( 𝐹 ∈ ( 𝐵 / ( ≃ph𝐽 ) ) ↔ ∃ 𝑓 𝐵 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) )
16 8 14 15 pm5.21nii ( 𝐹 ∈ ( 𝐵 / ( ≃ph𝐽 ) ) ↔ ∃ 𝑓 𝐵 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) )
17 1 3 4 5 pi1eluni ( 𝜑 → ( 𝑓 𝐵 ↔ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) )
18 3anass ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ↔ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) )
19 17 18 bitrdi ( 𝜑 → ( 𝑓 𝐵 ↔ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) ) )
20 19 anbi1d ( 𝜑 → ( ( 𝑓 𝐵𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ↔ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ) )
21 anass ( ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ↔ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ) )
22 20 21 bitrdi ( 𝜑 → ( ( 𝑓 𝐵𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ↔ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ) ) )
23 22 rexbidv2 ( 𝜑 → ( ∃ 𝑓 𝐵 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ) )
24 16 23 syl5bb ( 𝜑 → ( 𝐹 ∈ ( 𝐵 / ( ≃ph𝐽 ) ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ) )
25 7 24 bitrd ( 𝜑 → ( 𝐹𝐵 ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph𝐽 ) ) ) )