Proof of Theorem pi1xfrcnvlem
| Step | Hyp | Ref
| Expression |
| 1 | | pi1xfr.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 | | ecexg 8749 |
. . . . 5
⊢ ((
≃ph‘𝐽) ∈ V → [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽) ∈ V) |
| 6 | 2, 5 | mp1i 13 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽) ∈ V) |
| 7 | 1, 4, 6 | fliftcnv 7331 |
. . 3
⊢ (𝜑 → ◡𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽), [𝑔]( ≃ph‘𝐽)〉)) |
| 8 | | pi1xfr.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) |
| 9 | | pi1xfr.i |
. . . . . . . . . . . 12
⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) |
| 10 | 9 | pcorevcl 25058 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0))) |
| 11 | 8, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0))) |
| 12 | 11 | simp1d 1143 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐽)) |
| 13 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → 𝐼 ∈ (II Cn 𝐽)) |
| 14 | | pi1xfr.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (𝐽 π1 (𝐹‘0)) |
| 15 | | pi1xfr.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 16 | | iitopon 24905 |
. . . . . . . . . . . . . 14
⊢ II ∈
(TopOn‘(0[,]1)) |
| 17 | | cnf2 23257 |
. . . . . . . . . . . . . 14
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (II Cn 𝐽)) → 𝐹:(0[,]1)⟶𝑋) |
| 18 | 16, 15, 8, 17 | mp3an2i 1468 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:(0[,]1)⟶𝑋) |
| 19 | | 0elunit 13509 |
. . . . . . . . . . . . 13
⊢ 0 ∈
(0[,]1) |
| 20 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(0[,]1)⟶𝑋 ∧ 0 ∈ (0[,]1)) →
(𝐹‘0) ∈ 𝑋) |
| 21 | 18, 19, 20 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘0) ∈ 𝑋) |
| 22 | | pi1xfr.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑃) |
| 23 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 = (Base‘𝑃)) |
| 24 | 14, 15, 21, 23 | pi1eluni 25075 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑔 ∈ ∪ 𝐵 ↔ (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = (𝐹‘0) ∧ (𝑔‘1) = (𝐹‘0)))) |
| 25 | 24 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = (𝐹‘0) ∧ (𝑔‘1) = (𝐹‘0))) |
| 26 | 25 | simp1d 1143 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → 𝑔 ∈ (II Cn 𝐽)) |
| 27 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → 𝐹 ∈ (II Cn 𝐽)) |
| 28 | 25 | simp3d 1145 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝑔‘1) = (𝐹‘0)) |
| 29 | 26, 27, 28 | pcocn 25050 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝑔(*𝑝‘𝐽)𝐹) ∈ (II Cn 𝐽)) |
| 30 | 11 | simp3d 1145 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐼‘1) = (𝐹‘0)) |
| 31 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐼‘1) = (𝐹‘0)) |
| 32 | 25 | simp2d 1144 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝑔‘0) = (𝐹‘0)) |
| 33 | 31, 32 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐼‘1) = (𝑔‘0)) |
| 34 | 26, 27 | pco0 25047 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝑔(*𝑝‘𝐽)𝐹)‘0) = (𝑔‘0)) |
| 35 | 33, 34 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐼‘1) = ((𝑔(*𝑝‘𝐽)𝐹)‘0)) |
| 36 | 13, 29, 35 | pcocn 25050 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽)) |
| 37 | 13, 29 | pco0 25047 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))‘0) = (𝐼‘0)) |
| 38 | 11 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼‘0) = (𝐹‘1)) |
| 39 | 38 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐼‘0) = (𝐹‘1)) |
| 40 | 37, 39 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))‘0) = (𝐹‘1)) |
| 41 | 13, 29 | pco1 25048 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))‘1) = ((𝑔(*𝑝‘𝐽)𝐹)‘1)) |
| 42 | 26, 27 | pco1 25048 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝑔(*𝑝‘𝐽)𝐹)‘1) = (𝐹‘1)) |
| 43 | 41, 42 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))‘1) = (𝐹‘1)) |
| 44 | | pi1xfr.q |
. . . . . . . . 9
⊢ 𝑄 = (𝐽 π1 (𝐹‘1)) |
| 45 | | 1elunit 13510 |
. . . . . . . . . 10
⊢ 1 ∈
(0[,]1) |
| 46 | | ffvelcdm 7101 |
. . . . . . . . . 10
⊢ ((𝐹:(0[,]1)⟶𝑋 ∧ 1 ∈ (0[,]1)) →
(𝐹‘1) ∈ 𝑋) |
| 47 | 18, 45, 46 | sylancl 586 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘1) ∈ 𝑋) |
| 48 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑄) = (Base‘𝑄)) |
| 49 | 44, 15, 47, 48 | pi1eluni 25075 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) ∈ ∪
(Base‘𝑄) ↔
((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽) ∧ ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))‘0) = (𝐹‘1) ∧ ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))‘1) = (𝐹‘1)))) |
| 50 | 49 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) ∈ ∪
(Base‘𝑄) ↔
((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) ∈ (II Cn 𝐽) ∧ ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))‘0) = (𝐹‘1) ∧ ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))‘1) = (𝐹‘1)))) |
| 51 | 36, 40, 43, 50 | mpbir3and 1343 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) ∈ ∪
(Base‘𝑄)) |
| 52 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑔 ∈ ∪ 𝐵 ↦ (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))) = (𝑔 ∈ ∪ 𝐵 ↦ (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)))) |
| 53 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) = (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉)) |
| 54 | | eceq1 8784 |
. . . . . . 7
⊢ (ℎ = (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) → [ℎ]( ≃ph‘𝐽) = [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)) |
| 55 | | oveq1 7438 |
. . . . . . . . 9
⊢ (ℎ = (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) → (ℎ(*𝑝‘𝐽)𝐼) = ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼)) |
| 56 | 55 | oveq2d 7447 |
. . . . . . . 8
⊢ (ℎ = (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) → (𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼)) = (𝐹(*𝑝‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼))) |
| 57 | 56 | eceq1d 8785 |
. . . . . . 7
⊢ (ℎ = (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) → [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽) = [(𝐹(*𝑝‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)) |
| 58 | 54, 57 | opeq12d 4881 |
. . . . . 6
⊢ (ℎ = (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) → 〈[ℎ]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉 = 〈[(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) |
| 59 | 51, 52, 53, 58 | fmptco 7149 |
. . . . 5
⊢ (𝜑 → ((ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ∘ (𝑔 ∈ ∪ 𝐵
↦ (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)))) = (𝑔 ∈ ∪ 𝐵 ↦ 〈[(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉)) |
| 60 | | phtpcer 25027 |
. . . . . . . . 9
⊢ (
≃ph‘𝐽) Er (II Cn 𝐽) |
| 61 | 60 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (
≃ph‘𝐽) Er (II Cn 𝐽)) |
| 62 | 13, 26 | pco0 25047 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)𝑔)‘0) = (𝐼‘0)) |
| 63 | 62, 39 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐹‘1) = ((𝐼(*𝑝‘𝐽)𝑔)‘0)) |
| 64 | 61, 27 | erref 8765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → 𝐹( ≃ph‘𝐽)𝐹) |
| 65 | 61, 13 | erref 8765 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → 𝐼( ≃ph‘𝐽)𝐼) |
| 66 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ ((0[,]1)
× {(𝐹‘0)}) =
((0[,]1) × {(𝐹‘0)}) |
| 67 | 66 | pcopt2 25056 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘1) = (𝐹‘0)) → (𝑔(*𝑝‘𝐽)((0[,]1) × {(𝐹‘0)}))(
≃ph‘𝐽)𝑔) |
| 68 | 26, 28, 67 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝑔(*𝑝‘𝐽)((0[,]1) × {(𝐹‘0)}))(
≃ph‘𝐽)𝑔) |
| 69 | 39 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐹‘1) = (𝐼‘0)) |
| 70 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) |
| 71 | 26, 27, 13, 28, 69, 70 | pcoass 25057 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝑔(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)𝐼)( ≃ph‘𝐽)(𝑔(*𝑝‘𝐽)(𝐹(*𝑝‘𝐽)𝐼))) |
| 72 | 27, 13 | pco0 25047 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)‘0) = (𝐹‘0)) |
| 73 | 28, 72 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝑔‘1) = ((𝐹(*𝑝‘𝐽)𝐼)‘0)) |
| 74 | 61, 26 | erref 8765 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → 𝑔( ≃ph‘𝐽)𝑔) |
| 75 | 9, 66 | pcorev2 25061 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐼)( ≃ph‘𝐽)((0[,]1) × {(𝐹‘0)})) |
| 76 | 27, 75 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐹(*𝑝‘𝐽)𝐼)( ≃ph‘𝐽)((0[,]1) × {(𝐹‘0)})) |
| 77 | 73, 74, 76 | pcohtpy 25053 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝑔(*𝑝‘𝐽)(𝐹(*𝑝‘𝐽)𝐼))( ≃ph‘𝐽)(𝑔(*𝑝‘𝐽)((0[,]1) × {(𝐹‘0)}))) |
| 78 | 61, 71, 77 | ertr2d 8762 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝑔(*𝑝‘𝐽)((0[,]1) × {(𝐹‘0)}))(
≃ph‘𝐽)((𝑔(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)𝐼)) |
| 79 | 61, 68, 78 | ertr3d 8763 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → 𝑔( ≃ph‘𝐽)((𝑔(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)𝐼)) |
| 80 | 33, 65, 79 | pcohtpy 25053 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)𝑔)( ≃ph‘𝐽)(𝐼(*𝑝‘𝐽)((𝑔(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)𝐼))) |
| 81 | 42, 39 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝑔(*𝑝‘𝐽)𝐹)‘1) = (𝐼‘0)) |
| 82 | 13, 29, 13, 35, 81, 70 | pcoass 25057 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼)( ≃ph‘𝐽)(𝐼(*𝑝‘𝐽)((𝑔(*𝑝‘𝐽)𝐹)(*𝑝‘𝐽)𝐼))) |
| 83 | 61, 80, 82 | ertr4d 8764 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐼(*𝑝‘𝐽)𝑔)( ≃ph‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼)) |
| 84 | 63, 64, 83 | pcohtpy 25053 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐹(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)𝑔))( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼))) |
| 85 | 27, 13, 26, 69, 33, 70 | pcoass 25057 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)(*𝑝‘𝐽)𝑔)( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)𝑔))) |
| 86 | 27, 13 | pco1 25048 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)‘1) = (𝐼‘1)) |
| 87 | 86, 33 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)‘1) = (𝑔‘0)) |
| 88 | 87, 76, 74 | pcohtpy 25053 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)(*𝑝‘𝐽)𝑔)( ≃ph‘𝐽)(((0[,]1) × {(𝐹‘0)})(*𝑝‘𝐽)𝑔)) |
| 89 | 66 | pcopt 25055 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ (II Cn 𝐽) ∧ (𝑔‘0) = (𝐹‘0)) → (((0[,]1) × {(𝐹‘0)})(*𝑝‘𝐽)𝑔)( ≃ph‘𝐽)𝑔) |
| 90 | 26, 32, 89 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (((0[,]1) ×
{(𝐹‘0)})(*𝑝‘𝐽)𝑔)( ≃ph‘𝐽)𝑔) |
| 91 | 61, 88, 90 | ertrd 8761 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → ((𝐹(*𝑝‘𝐽)𝐼)(*𝑝‘𝐽)𝑔)( ≃ph‘𝐽)𝑔) |
| 92 | 61, 85, 91 | ertr3d 8763 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐹(*𝑝‘𝐽)(𝐼(*𝑝‘𝐽)𝑔))( ≃ph‘𝐽)𝑔) |
| 93 | 61, 84, 92 | ertr3d 8763 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → (𝐹(*𝑝‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼))( ≃ph‘𝐽)𝑔) |
| 94 | 61, 93 | erthi 8798 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → [(𝐹(*𝑝‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽) = [𝑔]( ≃ph‘𝐽)) |
| 95 | 94 | opeq2d 4880 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 ∈ ∪ 𝐵) → 〈[(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉 = 〈[(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽), [𝑔]( ≃ph‘𝐽)〉) |
| 96 | 95 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑔 ∈ ∪ 𝐵 ↦ 〈[(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)((𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) = (𝑔 ∈ ∪ 𝐵 ↦ 〈[(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽), [𝑔]( ≃ph‘𝐽)〉)) |
| 97 | 59, 96 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ((ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ∘ (𝑔 ∈ ∪ 𝐵
↦ (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)))) = (𝑔 ∈ ∪ 𝐵 ↦ 〈[(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽), [𝑔]( ≃ph‘𝐽)〉)) |
| 98 | 97 | rneqd 5949 |
. . 3
⊢ (𝜑 → ran ((ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ∘ (𝑔 ∈ ∪ 𝐵
↦ (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)))) = ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽), [𝑔]( ≃ph‘𝐽)〉)) |
| 99 | 7, 98 | eqtr4d 2780 |
. 2
⊢ (𝜑 → ◡𝐺 = ran ((ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ∘ (𝑔 ∈ ∪ 𝐵
↦ (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))))) |
| 100 | | rncoss 5986 |
. . 3
⊢ ran
((ℎ ∈ ∪ (Base‘𝑄) ↦ 〈[ℎ]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ∘ (𝑔 ∈ ∪ 𝐵
↦ (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)))) ⊆ ran (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) |
| 101 | | pi1xfrcnv.h |
. . 3
⊢ 𝐻 = ran (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) |
| 102 | 100, 101 | sseqtrri 4033 |
. 2
⊢ ran
((ℎ ∈ ∪ (Base‘𝑄) ↦ 〈[ℎ]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ∘ (𝑔 ∈ ∪ 𝐵
↦ (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)))) ⊆ 𝐻 |
| 103 | 99, 102 | eqsstrdi 4028 |
1
⊢ (𝜑 → ◡𝐺 ⊆ 𝐻) |