| Step | Hyp | Ref
| Expression |
| 1 | | efmnd.1 |
. 2
⊢ 𝐺 = (EndoFMnd‘𝐴) |
| 2 | | elex 3501 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
| 3 | | ovexd 7466 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑎 ↑m 𝑎) ∈ V) |
| 4 | | id 22 |
. . . . . . . 8
⊢ (𝑏 = (𝑎 ↑m 𝑎) → 𝑏 = (𝑎 ↑m 𝑎)) |
| 5 | | id 22 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
| 6 | 5, 5 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑎 ↑m 𝑎) = (𝐴 ↑m 𝐴)) |
| 7 | | efmnd.2 |
. . . . . . . . 9
⊢ 𝐵 = (𝐴 ↑m 𝐴) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎 ↑m 𝑎) = 𝐵) |
| 9 | 4, 8 | sylan9eqr 2799 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → 𝑏 = 𝐵) |
| 10 | 9 | opeq2d 4880 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐵〉) |
| 11 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔)) |
| 12 | 9, 9, 11 | mpoeq123dv 7508 |
. . . . . . . 8
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))) |
| 13 | | efmnd.3 |
. . . . . . . 8
⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) |
| 14 | 12, 13 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔)) = + ) |
| 15 | 14 | opeq2d 4880 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → 〈(+g‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))〉 = 〈(+g‘ndx),
+
〉) |
| 16 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → 𝑎 = 𝐴) |
| 17 | | pweq 4614 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴) |
| 18 | 17 | sneqd 4638 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → {𝒫 𝑎} = {𝒫 𝐴}) |
| 19 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → {𝒫 𝑎} = {𝒫 𝐴}) |
| 20 | 16, 19 | xpeq12d 5716 |
. . . . . . . . 9
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → (𝑎 × {𝒫 𝑎}) = (𝐴 × {𝒫 𝐴})) |
| 21 | 20 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → (∏t‘(𝑎 × {𝒫 𝑎})) =
(∏t‘(𝐴 × {𝒫 𝐴}))) |
| 22 | | efmnd.4 |
. . . . . . . 8
⊢ 𝐽 =
(∏t‘(𝐴 × {𝒫 𝐴})) |
| 23 | 21, 22 | eqtr4di 2795 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → (∏t‘(𝑎 × {𝒫 𝑎})) = 𝐽) |
| 24 | 23 | opeq2d 4880 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → 〈(TopSet‘ndx),
(∏t‘(𝑎 × {𝒫 𝑎}))〉 = 〈(TopSet‘ndx), 𝐽〉) |
| 25 | 10, 15, 24 | tpeq123d 4748 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = (𝑎 ↑m 𝑎)) → {〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝑎 × {𝒫 𝑎}))〉} = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
| 26 | 3, 25 | csbied 3935 |
. . . 4
⊢ (𝑎 = 𝐴 → ⦋(𝑎 ↑m 𝑎) / 𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝑎 × {𝒫 𝑎}))〉} = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
| 27 | | df-efmnd 18882 |
. . . 4
⊢ EndoFMnd
= (𝑎 ∈ V ↦
⦋(𝑎
↑m 𝑎) /
𝑏⦌{〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx),
(∏t‘(𝑎 × {𝒫 𝑎}))〉}) |
| 28 | | tpex 7766 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉} ∈ V |
| 29 | 26, 27, 28 | fvmpt 7016 |
. . 3
⊢ (𝐴 ∈ V →
(EndoFMnd‘𝐴) =
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
+ 〉,
〈(TopSet‘ndx), 𝐽〉}) |
| 30 | 2, 29 | syl 17 |
. 2
⊢ (𝐴 ∈ 𝑉 → (EndoFMnd‘𝐴) = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |
| 31 | 1, 30 | eqtrid 2789 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐺 = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(TopSet‘ndx), 𝐽〉}) |