| Step | Hyp | Ref | 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‘𝐽)〉) | 
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | pi1xfrcnvlem 25089 | . . 3
⊢ (𝜑 → ◡𝐺 ⊆ 𝐻) | 
| 10 |  | fvex 6919 | . . . . . . . 8
⊢ (
≃ph‘𝐽) ∈ V | 
| 11 |  | ecexg 8749 | . . . . . . . 8
⊢ ((
≃ph‘𝐽) ∈ V → [ℎ]( ≃ph‘𝐽) ∈ V) | 
| 12 | 10, 11 | mp1i 13 | . . . . . . 7
⊢ ((𝜑 ∧ ℎ ∈ ∪
(Base‘𝑄)) →
[ℎ](
≃ph‘𝐽) ∈ V) | 
| 13 |  | ecexg 8749 | . . . . . . . 8
⊢ ((
≃ph‘𝐽) ∈ V → [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽) ∈ V) | 
| 14 | 10, 13 | mp1i 13 | . . . . . . 7
⊢ ((𝜑 ∧ ℎ ∈ ∪
(Base‘𝑄)) →
[(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽) ∈ V) | 
| 15 | 8, 12, 14 | fliftrel 7328 | . . . . . 6
⊢ (𝜑 → 𝐻 ⊆ (V × V)) | 
| 16 |  | df-rel 5692 | . . . . . 6
⊢ (Rel
𝐻 ↔ 𝐻 ⊆ (V × V)) | 
| 17 | 15, 16 | sylibr 234 | . . . . 5
⊢ (𝜑 → Rel 𝐻) | 
| 18 |  | dfrel2 6209 | . . . . 5
⊢ (Rel
𝐻 ↔ ◡◡𝐻 = 𝐻) | 
| 19 | 17, 18 | sylib 218 | . . . 4
⊢ (𝜑 → ◡◡𝐻 = 𝐻) | 
| 20 |  | 0elunit 13509 | . . . . . . . . . 10
⊢ 0 ∈
(0[,]1) | 
| 21 |  | oveq2 7439 | . . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (1 − 𝑥) = (1 −
0)) | 
| 22 |  | 1m0e1 12387 | . . . . . . . . . . . . 13
⊢ (1
− 0) = 1 | 
| 23 | 21, 22 | eqtrdi 2793 | . . . . . . . . . . . 12
⊢ (𝑥 = 0 → (1 − 𝑥) = 1) | 
| 24 | 23 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝐹‘(1 − 𝑥)) = (𝐹‘1)) | 
| 25 |  | fvex 6919 | . . . . . . . . . . 11
⊢ (𝐹‘1) ∈
V | 
| 26 | 24, 7, 25 | fvmpt 7016 | . . . . . . . . . 10
⊢ (0 ∈
(0[,]1) → (𝐼‘0)
= (𝐹‘1)) | 
| 27 | 20, 26 | ax-mp 5 | . . . . . . . . 9
⊢ (𝐼‘0) = (𝐹‘1) | 
| 28 | 27 | oveq2i 7442 | . . . . . . . 8
⊢ (𝐽 π1 (𝐼‘0)) = (𝐽 π1 (𝐹‘1)) | 
| 29 | 2, 28 | eqtr4i 2768 | . . . . . . 7
⊢ 𝑄 = (𝐽 π1 (𝐼‘0)) | 
| 30 |  | 1elunit 13510 | . . . . . . . . . 10
⊢ 1 ∈
(0[,]1) | 
| 31 |  | oveq2 7439 | . . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (1 − 𝑥) = (1 −
1)) | 
| 32 | 31 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝐹‘(1 − 𝑥)) = (𝐹‘(1 − 1))) | 
| 33 |  | 1m1e0 12338 | . . . . . . . . . . . . 13
⊢ (1
− 1) = 0 | 
| 34 | 33 | fveq2i 6909 | . . . . . . . . . . . 12
⊢ (𝐹‘(1 − 1)) = (𝐹‘0) | 
| 35 | 32, 34 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝐹‘(1 − 𝑥)) = (𝐹‘0)) | 
| 36 |  | fvex 6919 | . . . . . . . . . . 11
⊢ (𝐹‘0) ∈
V | 
| 37 | 35, 7, 36 | fvmpt 7016 | . . . . . . . . . 10
⊢ (1 ∈
(0[,]1) → (𝐼‘1)
= (𝐹‘0)) | 
| 38 | 30, 37 | ax-mp 5 | . . . . . . . . 9
⊢ (𝐼‘1) = (𝐹‘0) | 
| 39 | 38 | oveq2i 7442 | . . . . . . . 8
⊢ (𝐽 π1 (𝐼‘1)) = (𝐽 π1 (𝐹‘0)) | 
| 40 | 1, 39 | eqtr4i 2768 | . . . . . . 7
⊢ 𝑃 = (𝐽 π1 (𝐼‘1)) | 
| 41 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝑄) =
(Base‘𝑄) | 
| 42 |  | eqid 2737 | . . . . . . 7
⊢ ran
(ℎ ∈ ∪ (Base‘𝑄) ↦ 〈[ℎ]( ≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) = ran (ℎ ∈ ∪ (Base‘𝑄) ↦ 〈[ℎ]( ≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) | 
| 43 | 7 | pcorevcl 25058 | . . . . . . . . 9
⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0))) | 
| 44 | 6, 43 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐽) ∧ (𝐼‘0) = (𝐹‘1) ∧ (𝐼‘1) = (𝐹‘0))) | 
| 45 | 44 | simp1d 1143 | . . . . . . 7
⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐽)) | 
| 46 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑧 = 𝑦 → (1 − 𝑧) = (1 − 𝑦)) | 
| 47 | 46 | fveq2d 6910 | . . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝐼‘(1 − 𝑧)) = (𝐼‘(1 − 𝑦))) | 
| 48 | 47 | cbvmptv 5255 | . . . . . . 7
⊢ (𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))) = (𝑦 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑦))) | 
| 49 |  | eqid 2737 | . . . . . . 7
⊢ ran
(𝑔 ∈ ∪ (Base‘𝑃) ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))](
≃ph‘𝐽)〉) = ran (𝑔 ∈ ∪
(Base‘𝑃) ↦
〈[𝑔](
≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))](
≃ph‘𝐽)〉) | 
| 50 | 29, 40, 41, 42, 5, 45, 48, 49 | pi1xfrcnvlem 25089 | . . . . . 6
⊢ (𝜑 → ◡ran (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ⊆ ran (𝑔 ∈ ∪ (Base‘𝑃) ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))](
≃ph‘𝐽)〉)) | 
| 51 |  | iitopon 24905 | . . . . . . . . . . . . . . . 16
⊢ II ∈
(TopOn‘(0[,]1)) | 
| 52 |  | cnf2 23257 | . . . . . . . . . . . . . . . 16
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (II Cn 𝐽)) → 𝐹:(0[,]1)⟶𝑋) | 
| 53 | 51, 5, 6, 52 | mp3an2i 1468 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:(0[,]1)⟶𝑋) | 
| 54 | 53 | feqmptd 6977 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 = (𝑧 ∈ (0[,]1) ↦ (𝐹‘𝑧))) | 
| 55 |  | iirev 24956 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (0[,]1) → (1
− 𝑧) ∈
(0[,]1)) | 
| 56 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (1 − 𝑧) → (1 − 𝑥) = (1 − (1 − 𝑧))) | 
| 57 | 56 | fveq2d 6910 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (1 − 𝑧) → (𝐹‘(1 − 𝑥)) = (𝐹‘(1 − (1 − 𝑧)))) | 
| 58 |  | fvex 6919 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐹‘(1 − (1 −
𝑧))) ∈
V | 
| 59 | 57, 7, 58 | fvmpt 7016 | . . . . . . . . . . . . . . . . 17
⊢ ((1
− 𝑧) ∈ (0[,]1)
→ (𝐼‘(1 −
𝑧)) = (𝐹‘(1 − (1 − 𝑧)))) | 
| 60 | 55, 59 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (0[,]1) → (𝐼‘(1 − 𝑧)) = (𝐹‘(1 − (1 − 𝑧)))) | 
| 61 |  | ax-1cn 11213 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ | 
| 62 |  | unitssre 13539 | . . . . . . . . . . . . . . . . . . . 20
⊢ (0[,]1)
⊆ ℝ | 
| 63 | 62 | sseli 3979 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (0[,]1) → 𝑧 ∈
ℝ) | 
| 64 | 63 | recnd 11289 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (0[,]1) → 𝑧 ∈
ℂ) | 
| 65 |  | nncan 11538 | . . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ 𝑧
∈ ℂ) → (1 − (1 − 𝑧)) = 𝑧) | 
| 66 | 61, 64, 65 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (0[,]1) → (1
− (1 − 𝑧)) =
𝑧) | 
| 67 | 66 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (0[,]1) → (𝐹‘(1 − (1 −
𝑧))) = (𝐹‘𝑧)) | 
| 68 | 60, 67 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (0[,]1) → (𝐼‘(1 − 𝑧)) = (𝐹‘𝑧)) | 
| 69 | 68 | mpteq2ia 5245 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))) = (𝑧 ∈ (0[,]1) ↦ (𝐹‘𝑧)) | 
| 70 | 54, 69 | eqtr4di 2795 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 = (𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))) | 
| 71 | 70 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼)) = ((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))) | 
| 72 | 71 | eceq1d 8785 | . . . . . . . . . . 11
⊢ (𝜑 → [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽) = [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)) | 
| 73 | 72 | opeq2d 4880 | . . . . . . . . . 10
⊢ (𝜑 → 〈[ℎ]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉 = 〈[ℎ](
≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) | 
| 74 | 73 | mpteq2dv 5244 | . . . . . . . . 9
⊢ (𝜑 → (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) = (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉)) | 
| 75 | 74 | rneqd 5949 | . . . . . . . 8
⊢ (𝜑 → ran (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) = ran (ℎ ∈ ∪ (Base‘𝑄) ↦ 〈[ℎ]( ≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉)) | 
| 76 | 8, 75 | eqtrid 2789 | . . . . . . 7
⊢ (𝜑 → 𝐻 = ran (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉)) | 
| 77 | 76 | cnveqd 5886 | . . . . . 6
⊢ (𝜑 → ◡𝐻 = ◡ran (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉)) | 
| 78 | 3 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 = (Base‘𝑃)) | 
| 79 | 78 | unieqd 4920 | . . . . . . . . 9
⊢ (𝜑 → ∪ 𝐵 =
∪ (Base‘𝑃)) | 
| 80 | 70 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑔(*𝑝‘𝐽)𝐹) = (𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧))))) | 
| 81 | 80 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹)) = (𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))) | 
| 82 | 81 | eceq1d 8785 | . . . . . . . . . 10
⊢ (𝜑 → [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽) = [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))](
≃ph‘𝐽)) | 
| 83 | 82 | opeq2d 4880 | . . . . . . . . 9
⊢ (𝜑 → 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉 = 〈[𝑔](
≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))](
≃ph‘𝐽)〉) | 
| 84 | 79, 83 | mpteq12dv 5233 | . . . . . . . 8
⊢ (𝜑 → (𝑔 ∈ ∪ 𝐵 ↦ 〈[𝑔](
≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉) = (𝑔 ∈ ∪
(Base‘𝑃) ↦
〈[𝑔](
≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))](
≃ph‘𝐽)〉)) | 
| 85 | 84 | rneqd 5949 | . . . . . . 7
⊢ (𝜑 → ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[𝑔](
≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉) = ran (𝑔 ∈ ∪ (Base‘𝑃) ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))](
≃ph‘𝐽)〉)) | 
| 86 | 4, 85 | eqtrid 2789 | . . . . . 6
⊢ (𝜑 → 𝐺 = ran (𝑔 ∈ ∪
(Base‘𝑃) ↦
〈[𝑔](
≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)(𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))))](
≃ph‘𝐽)〉)) | 
| 87 | 50, 77, 86 | 3sstr4d 4039 | . . . . 5
⊢ (𝜑 → ◡𝐻 ⊆ 𝐺) | 
| 88 |  | cnvss 5883 | . . . . 5
⊢ (◡𝐻 ⊆ 𝐺 → ◡◡𝐻 ⊆ ◡𝐺) | 
| 89 | 87, 88 | syl 17 | . . . 4
⊢ (𝜑 → ◡◡𝐻 ⊆ ◡𝐺) | 
| 90 | 19, 89 | eqsstrrd 4019 | . . 3
⊢ (𝜑 → 𝐻 ⊆ ◡𝐺) | 
| 91 | 9, 90 | eqssd 4001 | . 2
⊢ (𝜑 → ◡𝐺 = 𝐻) | 
| 92 | 91, 76 | eqtrd 2777 | . . 3
⊢ (𝜑 → ◡𝐺 = ran (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉)) | 
| 93 | 29, 40, 41, 42, 5, 45, 48 | pi1xfr 25088 | . . 3
⊢ (𝜑 → ran (ℎ ∈ ∪
(Base‘𝑄) ↦
〈[ℎ](
≃ph‘𝐽), [((𝑧 ∈ (0[,]1) ↦ (𝐼‘(1 − 𝑧)))(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ∈ (𝑄 GrpHom 𝑃)) | 
| 94 | 92, 93 | eqeltrd 2841 | . 2
⊢ (𝜑 → ◡𝐺 ∈ (𝑄 GrpHom 𝑃)) | 
| 95 | 91, 94 | jca 511 | 1
⊢ (𝜑 → (◡𝐺 = 𝐻 ∧ ◡𝐺 ∈ (𝑄 GrpHom 𝑃))) |