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

Theorem pi1xfrcnv 24420
Description: Given a path 𝐹 between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
Hypotheses
Ref Expression
pi1xfr.p 𝑃 = (𝐽 π1 (𝐹‘0))
pi1xfr.q 𝑄 = (𝐽 π1 (𝐹‘1))
pi1xfr.b 𝐵 = (Base‘𝑃)
pi1xfr.g 𝐺 = ran (𝑔 𝐵 ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽)⟩)
pi1xfr.j (𝜑𝐽 ∈ (TopOn‘𝑋))
pi1xfr.f (𝜑𝐹 ∈ (II Cn 𝐽))
pi1xfr.i 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))
pi1xfrcnv.h 𝐻 = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩)
Assertion
Ref Expression
pi1xfrcnv (𝜑 → (𝐺 = 𝐻𝐺 ∈ (𝑄 GrpHom 𝑃)))
Distinct variable groups:   𝑔,,𝑥,𝐵   𝑔,𝐹,,𝑥   𝑔,𝐼,,𝑥   ,𝐺   𝜑,𝑔,,𝑥   𝑔,𝐽,,𝑥   𝑃,𝑔,,𝑥   𝑄,𝑔,,𝑥
Allowed substitution hints:   𝐺(𝑥,𝑔)   𝐻(𝑥,𝑔,)   𝑋(𝑥,𝑔,)

Proof of Theorem pi1xfrcnv
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pi1xfr.p . . . 4 𝑃 = (𝐽 π1 (𝐹‘0))
2 pi1xfr.q . . . 4 𝑄 = (𝐽 π1 (𝐹‘1))
3 pi1xfr.b . . . 4 𝐵 = (Base‘𝑃)
4 pi1xfr.g . . . 4 𝐺 = ran (𝑔 𝐵 ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽)⟩)
5 pi1xfr.j . . . 4 (𝜑𝐽 ∈ (TopOn‘𝑋))
6 pi1xfr.f . . . 4 (𝜑𝐹 ∈ (II Cn 𝐽))
7 pi1xfr.i . . . 4 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥)))
8 pi1xfrcnv.h . . . 4 𝐻 = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩)
91, 2, 3, 4, 5, 6, 7, 8pi1xfrcnvlem 24419 . . 3 (𝜑𝐺𝐻)
10 fvex 6855 . . . . . . . 8 ( ≃ph𝐽) ∈ V
11 ecexg 8652 . . . . . . . 8 (( ≃ph𝐽) ∈ V → []( ≃ph𝐽) ∈ V)
1210, 11mp1i 13 . . . . . . 7 ((𝜑 (Base‘𝑄)) → []( ≃ph𝐽) ∈ V)
13 ecexg 8652 . . . . . . . 8 (( ≃ph𝐽) ∈ V → [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽) ∈ V)
1410, 13mp1i 13 . . . . . . 7 ((𝜑 (Base‘𝑄)) → [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽) ∈ V)
158, 12, 14fliftrel 7253 . . . . . 6 (𝜑𝐻 ⊆ (V × V))
16 df-rel 5640 . . . . . 6 (Rel 𝐻𝐻 ⊆ (V × V))
1715, 16sylibr 233 . . . . 5 (𝜑 → Rel 𝐻)
18 dfrel2 6141 . . . . 5 (Rel 𝐻𝐻 = 𝐻)
1917, 18sylib 217 . . . 4 (𝜑𝐻 = 𝐻)
20 0elunit 13386 . . . . . . . . . 10 0 ∈ (0[,]1)
21 oveq2 7365 . . . . . . . . . . . . 13 (𝑥 = 0 → (1 − 𝑥) = (1 − 0))
22 1m0e1 12274 . . . . . . . . . . . . 13 (1 − 0) = 1
2321, 22eqtrdi 2792 . . . . . . . . . . . 12 (𝑥 = 0 → (1 − 𝑥) = 1)
2423fveq2d 6846 . . . . . . . . . . 11 (𝑥 = 0 → (𝐹‘(1 − 𝑥)) = (𝐹‘1))
25 fvex 6855 . . . . . . . . . . 11 (𝐹‘1) ∈ V
2624, 7, 25fvmpt 6948 . . . . . . . . . 10 (0 ∈ (0[,]1) → (𝐼‘0) = (𝐹‘1))
2720, 26ax-mp 5 . . . . . . . . 9 (𝐼‘0) = (𝐹‘1)
2827oveq2i 7368 . . . . . . . 8 (𝐽 π1 (𝐼‘0)) = (𝐽 π1 (𝐹‘1))
292, 28eqtr4i 2767 . . . . . . 7 𝑄 = (𝐽 π1 (𝐼‘0))
30 1elunit 13387 . . . . . . . . . 10 1 ∈ (0[,]1)
31 oveq2 7365 . . . . . . . . . . . . 13 (𝑥 = 1 → (1 − 𝑥) = (1 − 1))
3231fveq2d 6846 . . . . . . . . . . . 12 (𝑥 = 1 → (𝐹‘(1 − 𝑥)) = (𝐹‘(1 − 1)))
33 1m1e0 12225 . . . . . . . . . . . . 13 (1 − 1) = 0
3433fveq2i 6845 . . . . . . . . . . . 12 (𝐹‘(1 − 1)) = (𝐹‘0)
3532, 34eqtrdi 2792 . . . . . . . . . . 11 (𝑥 = 1 → (𝐹‘(1 − 𝑥)) = (𝐹‘0))
36 fvex 6855 . . . . . . . . . . 11 (𝐹‘0) ∈ V
3735, 7, 36fvmpt 6948 . . . . . . . . . 10 (1 ∈ (0[,]1) → (𝐼‘1) = (𝐹‘0))
3830, 37ax-mp 5 . . . . . . . . 9 (𝐼‘1) = (𝐹‘0)
3938oveq2i 7368 . . . . . . . 8 (𝐽 π1 (𝐼‘1)) = (𝐽 π1 (𝐹‘0))
401, 39eqtr4i 2767 . . . . . . 7 𝑃 = (𝐽 π1 (𝐼‘1))
41 eqid 2736 . . . . . . 7 (Base‘𝑄) = (Base‘𝑄)
42 eqid 2736 . . . . . . 7 ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩)
437pcorevcl 24388 . . . . . . . . 9 (𝐹 ∈ (II Cn 𝐽) → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0)))
446, 43syl 17 . . . . . . . 8 (𝜑 → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0)))
4544simp1d 1142 . . . . . . 7 (𝜑𝐼 ∈ (II Cn 𝐽))
46 oveq2 7365 . . . . . . . . 9 (𝑧 = 𝑦 → (1 − 𝑧) = (1 − 𝑦))
4746fveq2d 6846 . . . . . . . 8 (𝑧 = 𝑦 → (𝐼‘(1 − 𝑧)) = (𝐼‘(1 − 𝑦)))
4847cbvmptv 5218 . . . . . . 7 (𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))) = (𝑦 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑦)))
49 eqid 2736 . . . . . . 7 ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩) = ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩)
5029, 40, 41, 42, 5, 45, 48, 49pi1xfrcnvlem 24419 . . . . . 6 (𝜑ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) ⊆ ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩))
51 iitopon 24242 . . . . . . . . . . . . . . . 16 II ∈ (TopOn‘(0[,]1))
52 cnf2 22600 . . . . . . . . . . . . . . . 16 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (II Cn 𝐽)) → 𝐹:(0[,]1)⟶𝑋)
5351, 5, 6, 52mp3an2i 1466 . . . . . . . . . . . . . . 15 (𝜑𝐹:(0[,]1)⟶𝑋)
5453feqmptd 6910 . . . . . . . . . . . . . 14 (𝜑𝐹 = (𝑧 ∈ (0[,]1) ↦ (𝐹𝑧)))
55 iirev 24292 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (0[,]1) → (1 − 𝑧) ∈ (0[,]1))
56 oveq2 7365 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (1 − 𝑧) → (1 − 𝑥) = (1 − (1 − 𝑧)))
5756fveq2d 6846 . . . . . . . . . . . . . . . . . 18 (𝑥 = (1 − 𝑧) → (𝐹‘(1 − 𝑥)) = (𝐹‘(1 − (1 − 𝑧))))
58 fvex 6855 . . . . . . . . . . . . . . . . . 18 (𝐹‘(1 − (1 − 𝑧))) ∈ V
5957, 7, 58fvmpt 6948 . . . . . . . . . . . . . . . . 17 ((1 − 𝑧) ∈ (0[,]1) → (𝐼‘(1 − 𝑧)) = (𝐹‘(1 − (1 − 𝑧))))
6055, 59syl 17 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (0[,]1) → (𝐼‘(1 − 𝑧)) = (𝐹‘(1 − (1 − 𝑧))))
61 ax-1cn 11109 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
62 unitssre 13416 . . . . . . . . . . . . . . . . . . . 20 (0[,]1) ⊆ ℝ
6362sseli 3940 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (0[,]1) → 𝑧 ∈ ℝ)
6463recnd 11183 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (0[,]1) → 𝑧 ∈ ℂ)
65 nncan 11430 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (1 − (1 − 𝑧)) = 𝑧)
6661, 64, 65sylancr 587 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (0[,]1) → (1 − (1 − 𝑧)) = 𝑧)
6766fveq2d 6846 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (0[,]1) → (𝐹‘(1 − (1 − 𝑧))) = (𝐹𝑧))
6860, 67eqtrd 2776 . . . . . . . . . . . . . . 15 (𝑧 ∈ (0[,]1) → (𝐼‘(1 − 𝑧)) = (𝐹𝑧))
6968mpteq2ia 5208 . . . . . . . . . . . . . 14 (𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))) = (𝑧 ∈ (0[,]1) ↦ (𝐹𝑧))
7054, 69eqtr4di 2794 . . . . . . . . . . . . 13 (𝜑𝐹 = (𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))))
7170oveq1d 7372 . . . . . . . . . . . 12 (𝜑 → (𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼)) = ((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼)))
7271eceq1d 8687 . . . . . . . . . . 11 (𝜑 → [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽) = [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽))
7372opeq2d 4837 . . . . . . . . . 10 (𝜑 → ⟨[]( ≃ph𝐽), [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩ = ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩)
7473mpteq2dv 5207 . . . . . . . . 9 (𝜑 → ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) = ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
7574rneqd 5893 . . . . . . . 8 (𝜑 → ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
768, 75eqtrid 2788 . . . . . . 7 (𝜑𝐻 = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
7776cnveqd 5831 . . . . . 6 (𝜑𝐻 = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
783a1i 11 . . . . . . . . . 10 (𝜑𝐵 = (Base‘𝑃))
7978unieqd 4879 . . . . . . . . 9 (𝜑 𝐵 = (Base‘𝑃))
8070oveq2d 7373 . . . . . . . . . . . 12 (𝜑 → (𝑔(*𝑝𝐽)𝐹) = (𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))
8180oveq2d 7373 . . . . . . . . . . 11 (𝜑 → (𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹)) = (𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))))))
8281eceq1d 8687 . . . . . . . . . 10 (𝜑 → [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽) = [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽))
8382opeq2d 4837 . . . . . . . . 9 (𝜑 → ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽)⟩ = ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩)
8479, 83mpteq12dv 5196 . . . . . . . 8 (𝜑 → (𝑔 𝐵 ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽)⟩) = (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩))
8584rneqd 5893 . . . . . . 7 (𝜑 → ran (𝑔 𝐵 ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽)⟩) = ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩))
864, 85eqtrid 2788 . . . . . 6 (𝜑𝐺 = ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩))
8750, 77, 863sstr4d 3991 . . . . 5 (𝜑𝐻𝐺)
88 cnvss 5828 . . . . 5 (𝐻𝐺𝐻𝐺)
8987, 88syl 17 . . . 4 (𝜑𝐻𝐺)
9019, 89eqsstrrd 3983 . . 3 (𝜑𝐻𝐺)
919, 90eqssd 3961 . 2 (𝜑𝐺 = 𝐻)
9291, 76eqtrd 2776 . . 3 (𝜑𝐺 = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
9329, 40, 41, 42, 5, 45, 48pi1xfr 24418 . . 3 (𝜑 → ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) ∈ (𝑄 GrpHom 𝑃))
9492, 93eqeltrd 2838 . 2 (𝜑𝐺 ∈ (𝑄 GrpHom 𝑃))
9591, 94jca 512 1 (𝜑 → (𝐺 = 𝐻𝐺 ∈ (𝑄 GrpHom 𝑃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  Vcvv 3445  wss 3910  cop 4592   cuni 4865  cmpt 5188   × cxp 5631  ccnv 5632  ran crn 5634  Rel wrel 5638  wf 6492  cfv 6496  (class class class)co 7357  [cec 8646  cc 11049  cr 11050  0cc0 11051  1c1 11052  cmin 11385  [,]cicc 13267  Basecbs 17083   GrpHom cghm 19005  TopOnctopon 22259   Cn ccn 22575  IIcii 24238  phcphtpc 24332  *𝑝cpco 24363   π1 cpi1 24366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-ec 8650  df-qs 8654  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-icc 13271  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-qus 17391  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-grp 18751  df-mulg 18873  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-cn 22578  df-cnp 22579  df-tx 22913  df-hmeo 23106  df-xms 23673  df-ms 23674  df-tms 23675  df-ii 24240  df-htpy 24333  df-phtpy 24334  df-phtpc 24355  df-pco 24368  df-om1 24369  df-pi1 24371
This theorem is referenced by:  pi1xfrgim  24421
  Copyright terms: Public domain W3C validator