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 bitrid ⊢ φ → 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