MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pin Structured version   Visualization version   GIF version

Definition df-pin 24525
Description: Define the n-th homotopy group, which is formed by taking the 𝑛-th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the 𝑛-th loop space, which is the 𝑛 βˆ’ 1-th loop space. For 𝑛 = 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 𝑋. (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.)
Assertion
Ref Expression
df-pin Ο€n = (𝑗 ∈ Top, 𝑝 ∈ βˆͺ 𝑗 ↦ (𝑛 ∈ β„•0 ↦ ((1st β€˜((𝑗 Ω𝑛 𝑝)β€˜π‘›)) /s if(𝑛 = 0, {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ ∈ (II Cn 𝑗)((π‘“β€˜0) = π‘₯ ∧ (π‘“β€˜1) = 𝑦)}, ( ≃phβ€˜(TopOpenβ€˜(1st β€˜((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1)))))))))
Distinct variable group:   𝑓,𝑗,𝑛,𝑝,π‘₯,𝑦

Detailed syntax breakdown of Definition df-pin
StepHypRef Expression
1 cpin 24520 . 2 class Ο€n
2 vj . . 3 setvar 𝑗
3 vp . . 3 setvar 𝑝
4 ctop 22395 . . 3 class Top
52cv 1541 . . . 4 class 𝑗
65cuni 4909 . . 3 class βˆͺ 𝑗
7 vn . . . 4 setvar 𝑛
8 cn0 12472 . . . 4 class β„•0
97cv 1541 . . . . . . 7 class 𝑛
103cv 1541 . . . . . . . 8 class 𝑝
11 comn 24518 . . . . . . . 8 class Ω𝑛
125, 10, 11co 7409 . . . . . . 7 class (𝑗 Ω𝑛 𝑝)
139, 12cfv 6544 . . . . . 6 class ((𝑗 Ω𝑛 𝑝)β€˜π‘›)
14 c1st 7973 . . . . . 6 class 1st
1513, 14cfv 6544 . . . . 5 class (1st β€˜((𝑗 Ω𝑛 𝑝)β€˜π‘›))
16 cc0 11110 . . . . . . 7 class 0
179, 16wceq 1542 . . . . . 6 wff 𝑛 = 0
18 vf . . . . . . . . . . . 12 setvar 𝑓
1918cv 1541 . . . . . . . . . . 11 class 𝑓
2016, 19cfv 6544 . . . . . . . . . 10 class (π‘“β€˜0)
21 vx . . . . . . . . . . 11 setvar π‘₯
2221cv 1541 . . . . . . . . . 10 class π‘₯
2320, 22wceq 1542 . . . . . . . . 9 wff (π‘“β€˜0) = π‘₯
24 c1 11111 . . . . . . . . . . 11 class 1
2524, 19cfv 6544 . . . . . . . . . 10 class (π‘“β€˜1)
26 vy . . . . . . . . . . 11 setvar 𝑦
2726cv 1541 . . . . . . . . . 10 class 𝑦
2825, 27wceq 1542 . . . . . . . . 9 wff (π‘“β€˜1) = 𝑦
2923, 28wa 397 . . . . . . . 8 wff ((π‘“β€˜0) = π‘₯ ∧ (π‘“β€˜1) = 𝑦)
30 cii 24391 . . . . . . . . 9 class II
31 ccn 22728 . . . . . . . . 9 class Cn
3230, 5, 31co 7409 . . . . . . . 8 class (II Cn 𝑗)
3329, 18, 32wrex 3071 . . . . . . 7 wff βˆƒπ‘“ ∈ (II Cn 𝑗)((π‘“β€˜0) = π‘₯ ∧ (π‘“β€˜1) = 𝑦)
3433, 21, 26copab 5211 . . . . . 6 class {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ ∈ (II Cn 𝑗)((π‘“β€˜0) = π‘₯ ∧ (π‘“β€˜1) = 𝑦)}
35 cmin 11444 . . . . . . . . . . 11 class βˆ’
369, 24, 35co 7409 . . . . . . . . . 10 class (𝑛 βˆ’ 1)
3736, 12cfv 6544 . . . . . . . . 9 class ((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1))
3837, 14cfv 6544 . . . . . . . 8 class (1st β€˜((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1)))
39 ctopn 17367 . . . . . . . 8 class TopOpen
4038, 39cfv 6544 . . . . . . 7 class (TopOpenβ€˜(1st β€˜((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1))))
41 cphtpc 24485 . . . . . . 7 class ≃ph
4240, 41cfv 6544 . . . . . 6 class ( ≃phβ€˜(TopOpenβ€˜(1st β€˜((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1)))))
4317, 34, 42cif 4529 . . . . 5 class if(𝑛 = 0, {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ ∈ (II Cn 𝑗)((π‘“β€˜0) = π‘₯ ∧ (π‘“β€˜1) = 𝑦)}, ( ≃phβ€˜(TopOpenβ€˜(1st β€˜((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1))))))
44 cqus 17451 . . . . 5 class /s
4515, 43, 44co 7409 . . . 4 class ((1st β€˜((𝑗 Ω𝑛 𝑝)β€˜π‘›)) /s if(𝑛 = 0, {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ ∈ (II Cn 𝑗)((π‘“β€˜0) = π‘₯ ∧ (π‘“β€˜1) = 𝑦)}, ( ≃phβ€˜(TopOpenβ€˜(1st β€˜((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1)))))))
467, 8, 45cmpt 5232 . . 3 class (𝑛 ∈ β„•0 ↦ ((1st β€˜((𝑗 Ω𝑛 𝑝)β€˜π‘›)) /s if(𝑛 = 0, {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ ∈ (II Cn 𝑗)((π‘“β€˜0) = π‘₯ ∧ (π‘“β€˜1) = 𝑦)}, ( ≃phβ€˜(TopOpenβ€˜(1st β€˜((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1))))))))
472, 3, 4, 6, 46cmpo 7411 . 2 class (𝑗 ∈ Top, 𝑝 ∈ βˆͺ 𝑗 ↦ (𝑛 ∈ β„•0 ↦ ((1st β€˜((𝑗 Ω𝑛 𝑝)β€˜π‘›)) /s if(𝑛 = 0, {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ ∈ (II Cn 𝑗)((π‘“β€˜0) = π‘₯ ∧ (π‘“β€˜1) = 𝑦)}, ( ≃phβ€˜(TopOpenβ€˜(1st β€˜((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1)))))))))
481, 47wceq 1542 1 wff Ο€n = (𝑗 ∈ Top, 𝑝 ∈ βˆͺ 𝑗 ↦ (𝑛 ∈ β„•0 ↦ ((1st β€˜((𝑗 Ω𝑛 𝑝)β€˜π‘›)) /s if(𝑛 = 0, {⟨π‘₯, π‘¦βŸ© ∣ βˆƒπ‘“ ∈ (II Cn 𝑗)((π‘“β€˜0) = π‘₯ ∧ (π‘“β€˜1) = 𝑦)}, ( ≃phβ€˜(TopOpenβ€˜(1st β€˜((𝑗 Ω𝑛 𝑝)β€˜(𝑛 βˆ’ 1)))))))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator