Metamath Proof Explorer


Definition df-pin

Description: Define the n-th homotopy group, which is formed by taking the n -th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the n -th loop space, which is the n - 1 -th loop space. For n = 0 , since this is not well-defined we replace this relation with the path-connectedness relation, so that the 0 -th homotopy group is the set of path components of X . (Since the 0 -th loop space does not have a group operation, neither does the 0 -th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion df-pin πn = ( 𝑗 ∈ Top , 𝑝 𝑗 ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpin πn
1 vj 𝑗
2 ctop Top
3 vp 𝑝
4 1 cv 𝑗
5 4 cuni 𝑗
6 vn 𝑛
7 cn0 0
8 c1st 1st
9 comn Ω𝑛
10 3 cv 𝑝
11 4 10 9 co ( 𝑗 Ω𝑛 𝑝 )
12 6 cv 𝑛
13 12 11 cfv ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 )
14 13 8 cfv ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) )
15 cqus /s
16 cc0 0
17 12 16 wceq 𝑛 = 0
18 vx 𝑥
19 vy 𝑦
20 vf 𝑓
21 cii II
22 ccn Cn
23 21 4 22 co ( II Cn 𝑗 )
24 20 cv 𝑓
25 16 24 cfv ( 𝑓 ‘ 0 )
26 18 cv 𝑥
27 25 26 wceq ( 𝑓 ‘ 0 ) = 𝑥
28 c1 1
29 28 24 cfv ( 𝑓 ‘ 1 )
30 19 cv 𝑦
31 29 30 wceq ( 𝑓 ‘ 1 ) = 𝑦
32 27 31 wa ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 )
33 32 20 23 wrex 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 )
34 33 18 19 copab { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) }
35 cphtpc ph
36 ctopn TopOpen
37 cmin
38 12 28 37 co ( 𝑛 − 1 )
39 38 11 cfv ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) )
40 39 8 cfv ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) )
41 40 36 cfv ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) )
42 41 35 cfv ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) )
43 17 34 42 cif if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) )
44 14 43 15 co ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) )
45 6 7 44 cmpt ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) )
46 1 3 2 5 45 cmpo ( 𝑗 ∈ Top , 𝑝 𝑗 ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) ) )
47 0 46 wceq πn = ( 𝑗 ∈ Top , 𝑝 𝑗 ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ 𝑛 ) ) /s if ( 𝑛 = 0 , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } , ( ≃ph ‘ ( TopOpen ‘ ( 1st ‘ ( ( 𝑗 Ω𝑛 𝑝 ) ‘ ( 𝑛 − 1 ) ) ) ) ) ) ) ) )