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

Proof

Step Hyp Ref Expression
1 elpi1.g ⊢ 𝐺 = ( 𝐽 π1 𝑌 )
2 elpi1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 elpi1.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 elpi1.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
5 elpi1i.3 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
6 elpi1i.4 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 𝑌 )
7 elpi1i.5 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = 𝑌 )
8 eceq1 ⊢ ( 𝑓 = 𝐹 → [ 𝑓 ] ( ≃ph ‘ 𝐽 ) = [ 𝐹 ] ( ≃ph ‘ 𝐽 ) )
9 8 eqcomd ⊢ ( 𝑓 = 𝐹 → [ 𝐹 ] ( ≃ph ‘ 𝐽 ) = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) )
10 9 biantrud ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ↔ ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ [ 𝐹 ] ( ≃ph ‘ 𝐽 ) = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ) )
11 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
12 11 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 0 ) = 𝑌 ↔ ( 𝐹 ‘ 0 ) = 𝑌 ) )
13 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
14 13 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 1 ) = 𝑌 ↔ ( 𝐹 ‘ 1 ) = 𝑌 ) )
15 12 14 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ↔ ( ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ) )
16 10 15 bitr3d ⊢ ( 𝑓 = 𝐹 → ( ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ [ 𝐹 ] ( ≃ph ‘ 𝐽 ) = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ↔ ( ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ) )
17 16 rspcev ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐹 ‘ 0 ) = 𝑌 ∧ ( 𝐹 ‘ 1 ) = 𝑌 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ [ 𝐹 ] ( ≃ph ‘ 𝐽 ) = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) )
18 5 6 7 17 syl12anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ [ 𝐹 ] ( ≃ph ‘ 𝐽 ) = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) )
19 1 2 3 4 elpi1 ⊢ ( 𝜑 → ( [ 𝐹 ] ( ≃ph ‘ 𝐽 ) ∈ 𝐵 ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) ∧ [ 𝐹 ] ( ≃ph ‘ 𝐽 ) = [ 𝑓 ] ( ≃ph ‘ 𝐽 ) ) ) )
20 18 19 mpbird ⊢ ( 𝜑 → [ 𝐹 ] ( ≃ph ‘ 𝐽 ) ∈ 𝐵 )