Metamath Proof Explorer

Theorem pconnpi1

Description: All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses pconnpi1.x ⊢ X = ⋃ J
pconnpi1.p ⊢ P = J π 1 A
pconnpi1.q ⊢ Q = J π 1 B
pconnpi1.s ⊢ S = Base P
pconnpi1.t ⊢ T = Base Q
Assertion pconnpi1 ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X → P ≃ 𝑔 Q

Proof

Step Hyp Ref Expression
1 pconnpi1.x ⊢ X = ⋃ J
2 pconnpi1.p ⊢ P = J π 1 A
3 pconnpi1.q ⊢ Q = J π 1 B
4 pconnpi1.s ⊢ S = Base P
5 pconnpi1.t ⊢ T = Base Q
6 1 pconncn ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X → ∃ f ∈ II Cn J f ⁡ 0 = A ∧ f ⁡ 1 = B
7 eqid ⊢ J π 1 f ⁡ 0 = J π 1 f ⁡ 0
8 eqid ⊢ J π 1 f ⁡ 1 = J π 1 f ⁡ 1
9 eqid ⊢ Base J π 1 f ⁡ 0 = Base J π 1 f ⁡ 0
10 eqid ⊢ ran ⁡ h ∈ ⋃ Base J π 1 f ⁡ 0 ⟼ h ≃ ph ⁡ J x ∈ 0 1 ⟼ f ⁡ 1 − x * 𝑝 ⁡ J h * 𝑝 ⁡ J f ≃ ph ⁡ J = ran ⁡ h ∈ ⋃ Base J π 1 f ⁡ 0 ⟼ h ≃ ph ⁡ J x ∈ 0 1 ⟼ f ⁡ 1 − x * 𝑝 ⁡ J h * 𝑝 ⁡ J f ≃ ph ⁡ J
11 simpl1 ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → J ∈ PConn
12 pconntop ⊢ J ∈ PConn → J ∈ Top
13 11 12 syl ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → J ∈ Top
14 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
15 13 14 sylib ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → J ∈ TopOn ⁡ X
16 simprl ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → f ∈ II Cn J
17 oveq2 ⊢ x = y → 1 − x = 1 − y
18 17 fveq2d ⊢ x = y → f ⁡ 1 − x = f ⁡ 1 − y
19 18 cbvmptv ⊢ x ∈ 0 1 ⟼ f ⁡ 1 − x = y ∈ 0 1 ⟼ f ⁡ 1 − y
20 7 8 9 10 15 16 19 pi1xfrgim ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → ran ⁡ h ∈ ⋃ Base J π 1 f ⁡ 0 ⟼ h ≃ ph ⁡ J x ∈ 0 1 ⟼ f ⁡ 1 − x * 𝑝 ⁡ J h * 𝑝 ⁡ J f ≃ ph ⁡ J ∈ J π 1 f ⁡ 0 GrpIso J π 1 f ⁡ 1
21 simprrl ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → f ⁡ 0 = A
22 21 oveq2d ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → J π 1 f ⁡ 0 = J π 1 A
23 22 2 eqtr4di ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → J π 1 f ⁡ 0 = P
24 simprrr ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → f ⁡ 1 = B
25 24 oveq2d ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → J π 1 f ⁡ 1 = J π 1 B
26 25 3 eqtr4di ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → J π 1 f ⁡ 1 = Q
27 23 26 oveq12d ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → J π 1 f ⁡ 0 GrpIso J π 1 f ⁡ 1 = P GrpIso Q
28 20 27 eleqtrd ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → ran ⁡ h ∈ ⋃ Base J π 1 f ⁡ 0 ⟼ h ≃ ph ⁡ J x ∈ 0 1 ⟼ f ⁡ 1 − x * 𝑝 ⁡ J h * 𝑝 ⁡ J f ≃ ph ⁡ J ∈ P GrpIso Q
29 brgici ⊢ ran ⁡ h ∈ ⋃ Base J π 1 f ⁡ 0 ⟼ h ≃ ph ⁡ J x ∈ 0 1 ⟼ f ⁡ 1 − x * 𝑝 ⁡ J h * 𝑝 ⁡ J f ≃ ph ⁡ J ∈ P GrpIso Q → P ≃ 𝑔 Q
30 28 29 syl ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X ∧ f ∈ II Cn J ∧ f ⁡ 0 = A ∧ f ⁡ 1 = B → P ≃ 𝑔 Q
31 6 30 rexlimddv ⊢ J ∈ PConn ∧ A ∈ X ∧ B ∈ X → P ≃ 𝑔 Q