Step | Hyp | Ref
| Expression |
1 | | pi1co.g |
. . . 4
⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ 〈[𝑔](
≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)〉) |
2 | | fvex 6113 |
. . . . 5
⊢ (
≃ph‘𝐽) ∈ V |
3 | | ecexg 7633 |
. . . . 5
⊢ ((
≃ph‘𝐽) ∈ V → [𝑔]( ≃ph‘𝐽) ∈ V) |
4 | 2, 3 | mp1i 13 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → [𝑔]( ≃ph‘𝐽) ∈ V) |
5 | | pi1co.q |
. . . . 5
⊢ 𝑄 = (𝐾 π1 𝐵) |
6 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑄) =
(Base‘𝑄) |
7 | | pi1co.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
8 | | cntop2 20855 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
10 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 |
11 | 10 | toptopon 20548 |
. . . . . . 7
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
12 | 9, 11 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
14 | | pi1co.b |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) = 𝐵) |
15 | | pi1co.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
16 | | cnf2 20863 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶∪ 𝐾) |
17 | 15, 12, 7, 16 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑋⟶∪ 𝐾) |
18 | | pi1co.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
19 | 17, 18 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) ∈ ∪ 𝐾) |
20 | 14, 19 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ∪ 𝐾) |
21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐵 ∈ ∪ 𝐾) |
22 | | pi1co.p |
. . . . . . . . 9
⊢ 𝑃 = (𝐽 π1 𝐴) |
23 | | pi1co.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑃) |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 = (Base‘𝑃)) |
25 | 22, 15, 18, 24 | pi1eluni 22650 |
. . . . . . . 8
⊢ (𝜑 → (𝑔 ∈ ∪ 𝑉 ↔ (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴))) |
26 | 25 | biimpa 500 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴)) |
27 | 26 | simp1d 1066 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝑔 ∈ (II Cn 𝐽)) |
28 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
29 | | cnco 20880 |
. . . . . 6
⊢ ((𝑔 ∈ (II Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ 𝑔) ∈ (II Cn 𝐾)) |
30 | 27, 28, 29 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹 ∘ 𝑔) ∈ (II Cn 𝐾)) |
31 | | iitopon 22490 |
. . . . . . . . 9
⊢ II ∈
(TopOn‘(0[,]1)) |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → II ∈
(TopOn‘(0[,]1))) |
33 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐽 ∈ (TopOn‘𝑋)) |
34 | | cnf2 20863 |
. . . . . . . 8
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (II Cn 𝐽)) → 𝑔:(0[,]1)⟶𝑋) |
35 | 32, 33, 27, 34 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝑔:(0[,]1)⟶𝑋) |
36 | | 0elunit 12161 |
. . . . . . 7
⊢ 0 ∈
(0[,]1) |
37 | | fvco3 6185 |
. . . . . . 7
⊢ ((𝑔:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) →
((𝐹 ∘ 𝑔)‘0) = (𝐹‘(𝑔‘0))) |
38 | 35, 36, 37 | sylancl 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘0) = (𝐹‘(𝑔‘0))) |
39 | 26 | simp2d 1067 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝑔‘0) = 𝐴) |
40 | 39 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹‘(𝑔‘0)) = (𝐹‘𝐴)) |
41 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹‘𝐴) = 𝐵) |
42 | 38, 40, 41 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘0) = 𝐵) |
43 | | 1elunit 12162 |
. . . . . . 7
⊢ 1 ∈
(0[,]1) |
44 | | fvco3 6185 |
. . . . . . 7
⊢ ((𝑔:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) →
((𝐹 ∘ 𝑔)‘1) = (𝐹‘(𝑔‘1))) |
45 | 35, 43, 44 | sylancl 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘1) = (𝐹‘(𝑔‘1))) |
46 | 26 | simp3d 1068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝑔‘1) = 𝐴) |
47 | 46 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹‘(𝑔‘1)) = (𝐹‘𝐴)) |
48 | 45, 47, 41 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘1) = 𝐵) |
49 | 5, 6, 13, 21, 30, 42, 48 | elpi1i 22654 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾) ∈ (Base‘𝑄)) |
50 | | eceq1 7669 |
. . . 4
⊢ (𝑔 = ℎ → [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽)) |
51 | | coeq2 5202 |
. . . . 5
⊢ (𝑔 = ℎ → (𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ)) |
52 | 51 | eceq1d 7670 |
. . . 4
⊢ (𝑔 = ℎ → [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) |
53 | | phtpcer 22602 |
. . . . . 6
⊢ (
≃ph‘𝐾) Er (II Cn 𝐾) |
54 | 53 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (
≃ph‘𝐾) Er (II Cn 𝐾)) |
55 | | simpr3 1062 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽)) |
56 | | phtpcer 22602 |
. . . . . . . . 9
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |
57 | 56 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
58 | | simpr1 1060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝑔 ∈ ∪ 𝑉) |
59 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝑔 ∈ ∪ 𝑉 ↔ (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴))) |
60 | 58, 59 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴)) |
61 | 60 | simp1d 1066 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝑔 ∈ (II Cn 𝐽)) |
62 | 57, 61 | erth 7678 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝑔( ≃ph‘𝐽)ℎ ↔ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) |
63 | 55, 62 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝑔( ≃ph‘𝐽)ℎ) |
64 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
65 | 63, 64 | phtpcco2 22607 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝐹 ∘ 𝑔)( ≃ph‘𝐾)(𝐹 ∘ ℎ)) |
66 | 54, 65 | erthi 7680 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) |
67 | 1, 4, 49, 50, 52, 66 | fliftfund 6463 |
. . 3
⊢ (𝜑 → Fun 𝐺) |
68 | 1, 4, 49 | fliftf 6465 |
. . 3
⊢ (𝜑 → (Fun 𝐺 ↔ 𝐺:ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))⟶(Base‘𝑄))) |
69 | 67, 68 | mpbid 221 |
. 2
⊢ (𝜑 → 𝐺:ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))⟶(Base‘𝑄)) |
70 | 22, 15, 18, 24 | pi1bas2 22649 |
. . . 4
⊢ (𝜑 → 𝑉 = (∪ 𝑉 / (
≃ph‘𝐽))) |
71 | | df-qs 7635 |
. . . . 5
⊢ (∪ 𝑉
/ ( ≃ph‘𝐽)) = {𝑠 ∣ ∃𝑔 ∈ ∪ 𝑉𝑠 = [𝑔]( ≃ph‘𝐽)} |
72 | | eqid 2610 |
. . . . . 6
⊢ (𝑔 ∈ ∪ 𝑉
↦ [𝑔](
≃ph‘𝐽)) = (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽)) |
73 | 72 | rnmpt 5292 |
. . . . 5
⊢ ran
(𝑔 ∈ ∪ 𝑉
↦ [𝑔](
≃ph‘𝐽)) = {𝑠 ∣ ∃𝑔 ∈ ∪ 𝑉𝑠 = [𝑔]( ≃ph‘𝐽)} |
74 | 71, 73 | eqtr4i 2635 |
. . . 4
⊢ (∪ 𝑉
/ ( ≃ph‘𝐽)) = ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽)) |
75 | 70, 74 | syl6eq 2660 |
. . 3
⊢ (𝜑 → 𝑉 = ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))) |
76 | 75 | feq2d 5944 |
. 2
⊢ (𝜑 → (𝐺:𝑉⟶(Base‘𝑄) ↔ 𝐺:ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))⟶(Base‘𝑄))) |
77 | 69, 76 | mpbird 246 |
1
⊢ (𝜑 → 𝐺:𝑉⟶(Base‘𝑄)) |