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

Theorem pi1xfrcnv 25075
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 25074 . . 3 (𝜑𝐺𝐻)
10 fvex 6914 . . . . . . . 8 ( ≃ph𝐽) ∈ V
11 ecexg 8738 . . . . . . . 8 (( ≃ph𝐽) ∈ V → []( ≃ph𝐽) ∈ V)
1210, 11mp1i 13 . . . . . . 7 ((𝜑 (Base‘𝑄)) → []( ≃ph𝐽) ∈ V)
13 ecexg 8738 . . . . . . . 8 (( ≃ph𝐽) ∈ V → [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽) ∈ V)
1410, 13mp1i 13 . . . . . . 7 ((𝜑 (Base‘𝑄)) → [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽) ∈ V)
158, 12, 14fliftrel 7320 . . . . . 6 (𝜑𝐻 ⊆ (V × V))
16 df-rel 5689 . . . . . 6 (Rel 𝐻𝐻 ⊆ (V × V))
1715, 16sylibr 233 . . . . 5 (𝜑 → Rel 𝐻)
18 dfrel2 6200 . . . . 5 (Rel 𝐻𝐻 = 𝐻)
1917, 18sylib 217 . . . 4 (𝜑𝐻 = 𝐻)
20 0elunit 13500 . . . . . . . . . 10 0 ∈ (0[,]1)
21 oveq2 7432 . . . . . . . . . . . . 13 (𝑥 = 0 → (1 − 𝑥) = (1 − 0))
22 1m0e1 12385 . . . . . . . . . . . . 13 (1 − 0) = 1
2321, 22eqtrdi 2782 . . . . . . . . . . . 12 (𝑥 = 0 → (1 − 𝑥) = 1)
2423fveq2d 6905 . . . . . . . . . . 11 (𝑥 = 0 → (𝐹‘(1 − 𝑥)) = (𝐹‘1))
25 fvex 6914 . . . . . . . . . . 11 (𝐹‘1) ∈ V
2624, 7, 25fvmpt 7009 . . . . . . . . . 10 (0 ∈ (0[,]1) → (𝐼‘0) = (𝐹‘1))
2720, 26ax-mp 5 . . . . . . . . 9 (𝐼‘0) = (𝐹‘1)
2827oveq2i 7435 . . . . . . . 8 (𝐽 π1 (𝐼‘0)) = (𝐽 π1 (𝐹‘1))
292, 28eqtr4i 2757 . . . . . . 7 𝑄 = (𝐽 π1 (𝐼‘0))
30 1elunit 13501 . . . . . . . . . 10 1 ∈ (0[,]1)
31 oveq2 7432 . . . . . . . . . . . . 13 (𝑥 = 1 → (1 − 𝑥) = (1 − 1))
3231fveq2d 6905 . . . . . . . . . . . 12 (𝑥 = 1 → (𝐹‘(1 − 𝑥)) = (𝐹‘(1 − 1)))
33 1m1e0 12336 . . . . . . . . . . . . 13 (1 − 1) = 0
3433fveq2i 6904 . . . . . . . . . . . 12 (𝐹‘(1 − 1)) = (𝐹‘0)
3532, 34eqtrdi 2782 . . . . . . . . . . 11 (𝑥 = 1 → (𝐹‘(1 − 𝑥)) = (𝐹‘0))
36 fvex 6914 . . . . . . . . . . 11 (𝐹‘0) ∈ V
3735, 7, 36fvmpt 7009 . . . . . . . . . 10 (1 ∈ (0[,]1) → (𝐼‘1) = (𝐹‘0))
3830, 37ax-mp 5 . . . . . . . . 9 (𝐼‘1) = (𝐹‘0)
3938oveq2i 7435 . . . . . . . 8 (𝐽 π1 (𝐼‘1)) = (𝐽 π1 (𝐹‘0))
401, 39eqtr4i 2757 . . . . . . 7 𝑃 = (𝐽 π1 (𝐼‘1))
41 eqid 2726 . . . . . . 7 (Base‘𝑄) = (Base‘𝑄)
42 eqid 2726 . . . . . . 7 ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩)
437pcorevcl 25043 . . . . . . . . 9 (𝐹 ∈ (II Cn 𝐽) → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0)))
446, 43syl 17 . . . . . . . 8 (𝜑 → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0)))
4544simp1d 1139 . . . . . . 7 (𝜑𝐼 ∈ (II Cn 𝐽))
46 oveq2 7432 . . . . . . . . 9 (𝑧 = 𝑦 → (1 − 𝑧) = (1 − 𝑦))
4746fveq2d 6905 . . . . . . . 8 (𝑧 = 𝑦 → (𝐼‘(1 − 𝑧)) = (𝐼‘(1 − 𝑦)))
4847cbvmptv 5266 . . . . . . 7 (𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))) = (𝑦 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑦)))
49 eqid 2726 . . . . . . 7 ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩) = ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩)
5029, 40, 41, 42, 5, 45, 48, 49pi1xfrcnvlem 25074 . . . . . 6 (𝜑ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) ⊆ ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩))
51 iitopon 24890 . . . . . . . . . . . . . . . 16 II ∈ (TopOn‘(0[,]1))
52 cnf2 23244 . . . . . . . . . . . . . . . 16 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (II Cn 𝐽)) → 𝐹:(0[,]1)⟶𝑋)
5351, 5, 6, 52mp3an2i 1463 . . . . . . . . . . . . . . 15 (𝜑𝐹:(0[,]1)⟶𝑋)
5453feqmptd 6971 . . . . . . . . . . . . . 14 (𝜑𝐹 = (𝑧 ∈ (0[,]1) ↦ (𝐹𝑧)))
55 iirev 24941 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (0[,]1) → (1 − 𝑧) ∈ (0[,]1))
56 oveq2 7432 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (1 − 𝑧) → (1 − 𝑥) = (1 − (1 − 𝑧)))
5756fveq2d 6905 . . . . . . . . . . . . . . . . . 18 (𝑥 = (1 − 𝑧) → (𝐹‘(1 − 𝑥)) = (𝐹‘(1 − (1 − 𝑧))))
58 fvex 6914 . . . . . . . . . . . . . . . . . 18 (𝐹‘(1 − (1 − 𝑧))) ∈ V
5957, 7, 58fvmpt 7009 . . . . . . . . . . . . . . . . 17 ((1 − 𝑧) ∈ (0[,]1) → (𝐼‘(1 − 𝑧)) = (𝐹‘(1 − (1 − 𝑧))))
6055, 59syl 17 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (0[,]1) → (𝐼‘(1 − 𝑧)) = (𝐹‘(1 − (1 − 𝑧))))
61 ax-1cn 11216 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
62 unitssre 13530 . . . . . . . . . . . . . . . . . . . 20 (0[,]1) ⊆ ℝ
6362sseli 3975 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (0[,]1) → 𝑧 ∈ ℝ)
6463recnd 11292 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (0[,]1) → 𝑧 ∈ ℂ)
65 nncan 11539 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (1 − (1 − 𝑧)) = 𝑧)
6661, 64, 65sylancr 585 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (0[,]1) → (1 − (1 − 𝑧)) = 𝑧)
6766fveq2d 6905 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (0[,]1) → (𝐹‘(1 − (1 − 𝑧))) = (𝐹𝑧))
6860, 67eqtrd 2766 . . . . . . . . . . . . . . 15 (𝑧 ∈ (0[,]1) → (𝐼‘(1 − 𝑧)) = (𝐹𝑧))
6968mpteq2ia 5256 . . . . . . . . . . . . . 14 (𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))) = (𝑧 ∈ (0[,]1) ↦ (𝐹𝑧))
7054, 69eqtr4di 2784 . . . . . . . . . . . . 13 (𝜑𝐹 = (𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))))
7170oveq1d 7439 . . . . . . . . . . . 12 (𝜑 → (𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼)) = ((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼)))
7271eceq1d 8774 . . . . . . . . . . 11 (𝜑 → [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽) = [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽))
7372opeq2d 4886 . . . . . . . . . 10 (𝜑 → ⟨[]( ≃ph𝐽), [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩ = ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩)
7473mpteq2dv 5255 . . . . . . . . 9 (𝜑 → ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) = ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
7574rneqd 5944 . . . . . . . 8 (𝜑 → ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [(𝐹(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
768, 75eqtrid 2778 . . . . . . 7 (𝜑𝐻 = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
7776cnveqd 5882 . . . . . 6 (𝜑𝐻 = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
783a1i 11 . . . . . . . . . 10 (𝜑𝐵 = (Base‘𝑃))
7978unieqd 4926 . . . . . . . . 9 (𝜑 𝐵 = (Base‘𝑃))
8070oveq2d 7440 . . . . . . . . . . . 12 (𝜑 → (𝑔(*𝑝𝐽)𝐹) = (𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))
8180oveq2d 7440 . . . . . . . . . . 11 (𝜑 → (𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹)) = (𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))))))
8281eceq1d 8774 . . . . . . . . . 10 (𝜑 → [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽) = [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽))
8382opeq2d 4886 . . . . . . . . 9 (𝜑 → ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽)⟩ = ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩)
8479, 83mpteq12dv 5244 . . . . . . . 8 (𝜑 → (𝑔 𝐵 ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽)⟩) = (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩))
8584rneqd 5944 . . . . . . 7 (𝜑 → ran (𝑔 𝐵 ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)𝐹))]( ≃ph𝐽)⟩) = ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩))
864, 85eqtrid 2778 . . . . . 6 (𝜑𝐺 = ran (𝑔 (Base‘𝑃) ↦ ⟨[𝑔]( ≃ph𝐽), [(𝐼(*𝑝𝐽)(𝑔(*𝑝𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))]( ≃ph𝐽)⟩))
8750, 77, 863sstr4d 4027 . . . . 5 (𝜑𝐻𝐺)
88 cnvss 5879 . . . . 5 (𝐻𝐺𝐻𝐺)
8987, 88syl 17 . . . 4 (𝜑𝐻𝐺)
9019, 89eqsstrrd 4019 . . 3 (𝜑𝐻𝐺)
919, 90eqssd 3997 . 2 (𝜑𝐺 = 𝐻)
9291, 76eqtrd 2766 . . 3 (𝜑𝐺 = ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩))
9329, 40, 41, 42, 5, 45, 48pi1xfr 25073 . . 3 (𝜑 → ran ( (Base‘𝑄) ↦ ⟨[]( ≃ph𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝𝐽)((*𝑝𝐽)𝐼))]( ≃ph𝐽)⟩) ∈ (𝑄 GrpHom 𝑃))
9492, 93eqeltrd 2826 . 2 (𝜑𝐺 ∈ (𝑄 GrpHom 𝑃))
9591, 94jca 510 1 (𝜑 → (𝐺 = 𝐻𝐺 ∈ (𝑄 GrpHom 𝑃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1534  wcel 2099  Vcvv 3462  wss 3947  cop 4639   cuni 4913  cmpt 5236   × cxp 5680  ccnv 5681  ran crn 5683  Rel wrel 5687  wf 6550  cfv 6554  (class class class)co 7424  [cec 8732  cc 11156  cr 11157  0cc0 11158  1c1 11159  cmin 11494  [,]cicc 13381  Basecbs 17213   GrpHom cghm 19206  TopOnctopon 22903   Cn ccn 23219  IIcii 24886  phcphtpc 24986  *𝑝cpco 25018   π1 cpi1 25021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236  ax-addf 11237
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-tp 4638  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-iin 5004  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7690  df-om 7877  df-1st 8003  df-2nd 8004  df-supp 8175  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-er 8734  df-ec 8736  df-qs 8740  df-map 8857  df-ixp 8927  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-fsupp 9406  df-fi 9454  df-sup 9485  df-inf 9486  df-oi 9553  df-card 9982  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12611  df-dec 12730  df-uz 12875  df-q 12985  df-rp 13029  df-xneg 13146  df-xadd 13147  df-xmul 13148  df-ioo 13382  df-icc 13385  df-fz 13539  df-fzo 13682  df-seq 14022  df-exp 14082  df-hash 14348  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241  df-struct 17149  df-sets 17166  df-slot 17184  df-ndx 17196  df-base 17214  df-ress 17243  df-plusg 17279  df-mulr 17280  df-starv 17281  df-sca 17282  df-vsca 17283  df-ip 17284  df-tset 17285  df-ple 17286  df-ds 17288  df-unif 17289  df-hom 17290  df-cco 17291  df-rest 17437  df-topn 17438  df-0g 17456  df-gsum 17457  df-topgen 17458  df-pt 17459  df-prds 17462  df-xrs 17517  df-qtop 17522  df-imas 17523  df-qus 17524  df-xps 17525  df-mre 17599  df-mrc 17600  df-acs 17602  df-mgm 18633  df-sgrp 18712  df-mnd 18728  df-submnd 18774  df-grp 18931  df-mulg 19062  df-ghm 19207  df-cntz 19311  df-cmn 19780  df-psmet 21335  df-xmet 21336  df-met 21337  df-bl 21338  df-mopn 21339  df-cnfld 21344  df-top 22887  df-topon 22904  df-topsp 22926  df-bases 22940  df-cld 23014  df-cn 23222  df-cnp 23223  df-tx 23557  df-hmeo 23750  df-xms 24317  df-ms 24318  df-tms 24319  df-ii 24888  df-htpy 24987  df-phtpy 24988  df-phtpc 25009  df-pco 25023  df-om1 25024  df-pi1 25026
This theorem is referenced by:  pi1xfrgim  25076
  Copyright terms: Public domain W3C validator