Step | Hyp | Ref
| Expression |
1 | | pi1co.g |
. . . 4
⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ 〈[𝑔](
≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)〉) |
2 | | fvex 6681 |
. . . . 5
⊢ (
≃ph‘𝐽) ∈ V |
3 | | ecexg 8317 |
. . . . 5
⊢ ((
≃ph‘𝐽) ∈ V → [𝑔]( ≃ph‘𝐽) ∈ V) |
4 | 2, 3 | mp1i 13 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → [𝑔]( ≃ph‘𝐽) ∈ V) |
5 | | pi1co.q |
. . . . 5
⊢ 𝑄 = (𝐾 π1 𝐵) |
6 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑄) =
(Base‘𝑄) |
7 | | pi1co.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
8 | | cntop2 21985 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
10 | | toptopon2 21662 |
. . . . . . 7
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
11 | 9, 10 | sylib 221 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
12 | 11 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
13 | | pi1co.b |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) = 𝐵) |
14 | | pi1co.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
15 | | cnf2 21993 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶∪ 𝐾) |
16 | 14, 11, 7, 15 | syl3anc 1372 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑋⟶∪ 𝐾) |
17 | | pi1co.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
18 | 16, 17 | ffvelrnd 6856 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) ∈ ∪ 𝐾) |
19 | 13, 18 | eqeltrrd 2834 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ∪ 𝐾) |
20 | 19 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐵 ∈ ∪ 𝐾) |
21 | | pi1co.p |
. . . . . . . . 9
⊢ 𝑃 = (𝐽 π1 𝐴) |
22 | | pi1co.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑃) |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 = (Base‘𝑃)) |
24 | 21, 14, 17, 23 | pi1eluni 23787 |
. . . . . . . 8
⊢ (𝜑 → (𝑔 ∈ ∪ 𝑉 ↔ (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴))) |
25 | 24 | biimpa 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴)) |
26 | 25 | simp1d 1143 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝑔 ∈ (II Cn 𝐽)) |
27 | 7 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
28 | | cnco 22010 |
. . . . . 6
⊢ ((𝑔 ∈ (II Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ 𝑔) ∈ (II Cn 𝐾)) |
29 | 26, 27, 28 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹 ∘ 𝑔) ∈ (II Cn 𝐾)) |
30 | | iitopon 23624 |
. . . . . . . 8
⊢ II ∈
(TopOn‘(0[,]1)) |
31 | | cnf2 21993 |
. . . . . . . 8
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (II Cn 𝐽)) → 𝑔:(0[,]1)⟶𝑋) |
32 | 30, 14, 26, 31 | mp3an2ani 1469 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝑔:(0[,]1)⟶𝑋) |
33 | | 0elunit 12936 |
. . . . . . 7
⊢ 0 ∈
(0[,]1) |
34 | | fvco3 6761 |
. . . . . . 7
⊢ ((𝑔:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) →
((𝐹 ∘ 𝑔)‘0) = (𝐹‘(𝑔‘0))) |
35 | 32, 33, 34 | sylancl 589 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘0) = (𝐹‘(𝑔‘0))) |
36 | 25 | simp2d 1144 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝑔‘0) = 𝐴) |
37 | 36 | fveq2d 6672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹‘(𝑔‘0)) = (𝐹‘𝐴)) |
38 | 13 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹‘𝐴) = 𝐵) |
39 | 35, 37, 38 | 3eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘0) = 𝐵) |
40 | | 1elunit 12937 |
. . . . . . 7
⊢ 1 ∈
(0[,]1) |
41 | | fvco3 6761 |
. . . . . . 7
⊢ ((𝑔:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) →
((𝐹 ∘ 𝑔)‘1) = (𝐹‘(𝑔‘1))) |
42 | 32, 40, 41 | sylancl 589 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘1) = (𝐹‘(𝑔‘1))) |
43 | 25 | simp3d 1145 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝑔‘1) = 𝐴) |
44 | 43 | fveq2d 6672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹‘(𝑔‘1)) = (𝐹‘𝐴)) |
45 | 42, 44, 38 | 3eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘1) = 𝐵) |
46 | 5, 6, 12, 20, 29, 39, 45 | elpi1i 23791 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾) ∈ (Base‘𝑄)) |
47 | | eceq1 8351 |
. . . 4
⊢ (𝑔 = ℎ → [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽)) |
48 | | coeq2 5695 |
. . . . 5
⊢ (𝑔 = ℎ → (𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ)) |
49 | 48 | eceq1d 8352 |
. . . 4
⊢ (𝑔 = ℎ → [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) |
50 | | phtpcer 23740 |
. . . . . 6
⊢ (
≃ph‘𝐾) Er (II Cn 𝐾) |
51 | 50 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (
≃ph‘𝐾) Er (II Cn 𝐾)) |
52 | | simpr3 1197 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽)) |
53 | | phtpcer 23740 |
. . . . . . . . 9
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |
54 | 53 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
55 | | simpr1 1195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝑔 ∈ ∪ 𝑉) |
56 | 24 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝑔 ∈ ∪ 𝑉 ↔ (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴))) |
57 | 55, 56 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴)) |
58 | 57 | simp1d 1143 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝑔 ∈ (II Cn 𝐽)) |
59 | 54, 58 | erth 8362 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝑔( ≃ph‘𝐽)ℎ ↔ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) |
60 | 52, 59 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝑔( ≃ph‘𝐽)ℎ) |
61 | 7 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
62 | 60, 61 | phtpcco2 23744 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝐹 ∘ 𝑔)( ≃ph‘𝐾)(𝐹 ∘ ℎ)) |
63 | 51, 62 | erthi 8364 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) |
64 | 1, 4, 46, 47, 49, 63 | fliftfund 7073 |
. . 3
⊢ (𝜑 → Fun 𝐺) |
65 | 1, 4, 46 | fliftf 7075 |
. . 3
⊢ (𝜑 → (Fun 𝐺 ↔ 𝐺:ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))⟶(Base‘𝑄))) |
66 | 64, 65 | mpbid 235 |
. 2
⊢ (𝜑 → 𝐺:ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))⟶(Base‘𝑄)) |
67 | 21, 14, 17, 23 | pi1bas2 23786 |
. . . 4
⊢ (𝜑 → 𝑉 = (∪ 𝑉 / (
≃ph‘𝐽))) |
68 | | df-qs 8319 |
. . . . 5
⊢ (∪ 𝑉
/ ( ≃ph‘𝐽)) = {𝑠 ∣ ∃𝑔 ∈ ∪ 𝑉𝑠 = [𝑔]( ≃ph‘𝐽)} |
69 | | eqid 2738 |
. . . . . 6
⊢ (𝑔 ∈ ∪ 𝑉
↦ [𝑔](
≃ph‘𝐽)) = (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽)) |
70 | 69 | rnmpt 5792 |
. . . . 5
⊢ ran
(𝑔 ∈ ∪ 𝑉
↦ [𝑔](
≃ph‘𝐽)) = {𝑠 ∣ ∃𝑔 ∈ ∪ 𝑉𝑠 = [𝑔]( ≃ph‘𝐽)} |
71 | 68, 70 | eqtr4i 2764 |
. . . 4
⊢ (∪ 𝑉
/ ( ≃ph‘𝐽)) = ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽)) |
72 | 67, 71 | eqtrdi 2789 |
. . 3
⊢ (𝜑 → 𝑉 = ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))) |
73 | 72 | feq2d 6484 |
. 2
⊢ (𝜑 → (𝐺:𝑉⟶(Base‘𝑄) ↔ 𝐺:ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))⟶(Base‘𝑄))) |
74 | 66, 73 | mpbird 260 |
1
⊢ (𝜑 → 𝐺:𝑉⟶(Base‘𝑄)) |