| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pi1co.g | . . . 4
⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ 〈[𝑔](
≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)〉) | 
| 2 |  | fvex 6919 | . . . . 5
⊢ (
≃ph‘𝐽) ∈ V | 
| 3 |  | ecexg 8749 | . . . . 5
⊢ ((
≃ph‘𝐽) ∈ V → [𝑔]( ≃ph‘𝐽) ∈ V) | 
| 4 | 2, 3 | mp1i 13 | . . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → [𝑔]( ≃ph‘𝐽) ∈ V) | 
| 5 |  | pi1co.q | . . . . 5
⊢ 𝑄 = (𝐾 π1 𝐵) | 
| 6 |  | eqid 2737 | . . . . 5
⊢
(Base‘𝑄) =
(Base‘𝑄) | 
| 7 |  | pi1co.f | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 8 |  | cntop2 23249 | . . . . . . . 8
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) | 
| 9 | 7, 8 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 10 |  | toptopon2 22924 | . . . . . . 7
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 11 | 9, 10 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 12 | 11 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 13 |  | pi1co.b | . . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) = 𝐵) | 
| 14 |  | pi1co.j | . . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 15 |  | cnf2 23257 | . . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶∪ 𝐾) | 
| 16 | 14, 11, 7, 15 | syl3anc 1373 | . . . . . . . 8
⊢ (𝜑 → 𝐹:𝑋⟶∪ 𝐾) | 
| 17 |  | pi1co.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑋) | 
| 18 | 16, 17 | ffvelcdmd 7105 | . . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) ∈ ∪ 𝐾) | 
| 19 | 13, 18 | eqeltrrd 2842 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ ∪ 𝐾) | 
| 20 | 19 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐵 ∈ ∪ 𝐾) | 
| 21 |  | pi1co.p | . . . . . . . . 9
⊢ 𝑃 = (𝐽 π1 𝐴) | 
| 22 |  | pi1co.v | . . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑃) | 
| 23 | 22 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝑉 = (Base‘𝑃)) | 
| 24 | 21, 14, 17, 23 | pi1eluni 25075 | . . . . . . . 8
⊢ (𝜑 → (𝑔 ∈ ∪ 𝑉 ↔ (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴))) | 
| 25 | 24 | biimpa 476 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴)) | 
| 26 | 25 | simp1d 1143 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝑔 ∈ (II Cn 𝐽)) | 
| 27 | 7 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 28 |  | cnco 23274 | . . . . . 6
⊢ ((𝑔 ∈ (II Cn 𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ 𝑔) ∈ (II Cn 𝐾)) | 
| 29 | 26, 27, 28 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹 ∘ 𝑔) ∈ (II Cn 𝐾)) | 
| 30 |  | iitopon 24905 | . . . . . . . 8
⊢ II ∈
(TopOn‘(0[,]1)) | 
| 31 |  | cnf2 23257 | . . . . . . . 8
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝑔 ∈ (II Cn 𝐽)) → 𝑔:(0[,]1)⟶𝑋) | 
| 32 | 30, 14, 26, 31 | mp3an2ani 1470 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → 𝑔:(0[,]1)⟶𝑋) | 
| 33 |  | 0elunit 13509 | . . . . . . 7
⊢ 0 ∈
(0[,]1) | 
| 34 |  | fvco3 7008 | . . . . . . 7
⊢ ((𝑔:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) →
((𝐹 ∘ 𝑔)‘0) = (𝐹‘(𝑔‘0))) | 
| 35 | 32, 33, 34 | sylancl 586 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘0) = (𝐹‘(𝑔‘0))) | 
| 36 | 25 | simp2d 1144 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝑔‘0) = 𝐴) | 
| 37 | 36 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹‘(𝑔‘0)) = (𝐹‘𝐴)) | 
| 38 | 13 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹‘𝐴) = 𝐵) | 
| 39 | 35, 37, 38 | 3eqtrd 2781 | . . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘0) = 𝐵) | 
| 40 |  | 1elunit 13510 | . . . . . . 7
⊢ 1 ∈
(0[,]1) | 
| 41 |  | fvco3 7008 | . . . . . . 7
⊢ ((𝑔:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) →
((𝐹 ∘ 𝑔)‘1) = (𝐹‘(𝑔‘1))) | 
| 42 | 32, 40, 41 | sylancl 586 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘1) = (𝐹‘(𝑔‘1))) | 
| 43 | 25 | simp3d 1145 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝑔‘1) = 𝐴) | 
| 44 | 43 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → (𝐹‘(𝑔‘1)) = (𝐹‘𝐴)) | 
| 45 | 42, 44, 38 | 3eqtrd 2781 | . . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → ((𝐹 ∘ 𝑔)‘1) = 𝐵) | 
| 46 | 5, 6, 12, 20, 29, 39, 45 | elpi1i 25079 | . . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝑉) → [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾) ∈ (Base‘𝑄)) | 
| 47 |  | eceq1 8784 | . . . 4
⊢ (𝑔 = ℎ → [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽)) | 
| 48 |  | coeq2 5869 | . . . . 5
⊢ (𝑔 = ℎ → (𝐹 ∘ 𝑔) = (𝐹 ∘ ℎ)) | 
| 49 | 48 | eceq1d 8785 | . . . 4
⊢ (𝑔 = ℎ → [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) | 
| 50 |  | phtpcer 25027 | . . . . . 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 25027 | . . . . . . . . 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 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝑔 ∈ ∪ 𝑉 ↔ (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴))) | 
| 57 | 55, 56 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = 𝐴 ∧ (𝑔‘1) = 𝐴)) | 
| 58 | 57 | simp1d 1143 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝑔 ∈ (II Cn 𝐽)) | 
| 59 | 54, 58 | erth 8796 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝑔( ≃ph‘𝐽)ℎ ↔ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) | 
| 60 | 52, 59 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝑔( ≃ph‘𝐽)ℎ) | 
| 61 | 7 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 62 | 60, 61 | phtpcco2 25032 | . . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → (𝐹 ∘ 𝑔)( ≃ph‘𝐾)(𝐹 ∘ ℎ)) | 
| 63 | 51, 62 | erthi 8798 | . . . 4
⊢ ((𝜑 ∧ (𝑔 ∈ ∪ 𝑉 ∧ ℎ ∈ ∪ 𝑉 ∧ [𝑔]( ≃ph‘𝐽) = [ℎ]( ≃ph‘𝐽))) → [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾) = [(𝐹 ∘ ℎ)]( ≃ph‘𝐾)) | 
| 64 | 1, 4, 46, 47, 49, 63 | fliftfund 7333 | . . 3
⊢ (𝜑 → Fun 𝐺) | 
| 65 | 1, 4, 46 | fliftf 7335 | . . 3
⊢ (𝜑 → (Fun 𝐺 ↔ 𝐺:ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))⟶(Base‘𝑄))) | 
| 66 | 64, 65 | mpbid 232 | . 2
⊢ (𝜑 → 𝐺:ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))⟶(Base‘𝑄)) | 
| 67 | 21, 14, 17, 23 | pi1bas2 25074 | . . . 4
⊢ (𝜑 → 𝑉 = (∪ 𝑉 / (
≃ph‘𝐽))) | 
| 68 |  | df-qs 8751 | . . . . 5
⊢ (∪ 𝑉
/ ( ≃ph‘𝐽)) = {𝑠 ∣ ∃𝑔 ∈ ∪ 𝑉𝑠 = [𝑔]( ≃ph‘𝐽)} | 
| 69 |  | eqid 2737 | . . . . . 6
⊢ (𝑔 ∈ ∪ 𝑉
↦ [𝑔](
≃ph‘𝐽)) = (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽)) | 
| 70 | 69 | rnmpt 5968 | . . . . 5
⊢ ran
(𝑔 ∈ ∪ 𝑉
↦ [𝑔](
≃ph‘𝐽)) = {𝑠 ∣ ∃𝑔 ∈ ∪ 𝑉𝑠 = [𝑔]( ≃ph‘𝐽)} | 
| 71 | 68, 70 | eqtr4i 2768 | . . . 4
⊢ (∪ 𝑉
/ ( ≃ph‘𝐽)) = ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽)) | 
| 72 | 67, 71 | eqtrdi 2793 | . . 3
⊢ (𝜑 → 𝑉 = ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))) | 
| 73 | 72 | feq2d 6722 | . 2
⊢ (𝜑 → (𝐺:𝑉⟶(Base‘𝑄) ↔ 𝐺:ran (𝑔 ∈ ∪ 𝑉 ↦ [𝑔]( ≃ph‘𝐽))⟶(Base‘𝑄))) | 
| 74 | 66, 73 | mpbird 257 | 1
⊢ (𝜑 → 𝐺:𝑉⟶(Base‘𝑄)) |