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 bitrid ⊢ ( 𝜑 → ( 𝐹 ∈ ( ∪ 𝐵 / ( ≃ph ‘ 𝐽 ) ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ) )
25 7 24 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ 𝐵 ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ 𝐹 = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ) )