Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . . . . . . . 9
⊢
(mCN‘𝑇) ∈
V |
2 | | mrsubvr.v |
. . . . . . . . . 10
⊢ 𝑉 = (mVR‘𝑇) |
3 | | fvex 6201 |
. . . . . . . . . 10
⊢
(mVR‘𝑇) ∈
V |
4 | 2, 3 | eqeltri 2697 |
. . . . . . . . 9
⊢ 𝑉 ∈ V |
5 | 1, 4 | unex 6956 |
. . . . . . . 8
⊢
((mCN‘𝑇) ∪
𝑉) ∈
V |
6 | | eqid 2622 |
. . . . . . . . 9
⊢
(freeMnd‘((mCN‘𝑇) ∪ 𝑉)) = (freeMnd‘((mCN‘𝑇) ∪ 𝑉)) |
7 | 6 | frmdmnd 17396 |
. . . . . . . 8
⊢
(((mCN‘𝑇)
∪ 𝑉) ∈ V →
(freeMnd‘((mCN‘𝑇) ∪ 𝑉)) ∈ Mnd) |
8 | 5, 7 | mp1i 13 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) → (freeMnd‘((mCN‘𝑇) ∪ 𝑉)) ∈ Mnd) |
9 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) → 𝑒 ∈ 𝑅) |
10 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
11 | | mrsubvr.r |
. . . . . . . . . . 11
⊢ 𝑅 = (mREx‘𝑇) |
12 | 10, 2, 11 | mrexval 31398 |
. . . . . . . . . 10
⊢ (𝑇 ∈ 𝑊 → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
13 | 12 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
14 | 9, 13 | eleqtrd 2703 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) → 𝑒 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
15 | | elpmi 7876 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) → (𝑓:dom 𝑓⟶𝑅 ∧ dom 𝑓 ⊆ 𝑉)) |
16 | 15 | simpld 475 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) → 𝑓:dom 𝑓⟶𝑅) |
17 | 16 | ad3antlr 767 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉)) → 𝑓:dom 𝑓⟶𝑅) |
18 | 17 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢
(((((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉)) ∧ 𝑣 ∈ dom 𝑓) → (𝑓‘𝑣) ∈ 𝑅) |
19 | 13 | ad2antrr 762 |
. . . . . . . . . . 11
⊢
(((((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉)) ∧ 𝑣 ∈ dom 𝑓) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
20 | 18, 19 | eleqtrd 2703 |
. . . . . . . . . 10
⊢
(((((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉)) ∧ 𝑣 ∈ dom 𝑓) → (𝑓‘𝑣) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
21 | | simplr 792 |
. . . . . . . . . . 11
⊢
(((((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉)) ∧ ¬ 𝑣 ∈ dom 𝑓) → 𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉)) |
22 | 21 | s1cld 13383 |
. . . . . . . . . 10
⊢
(((((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉)) ∧ ¬ 𝑣 ∈ dom 𝑓) → 〈“𝑣”〉 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
23 | 20, 22 | ifclda 4120 |
. . . . . . . . 9
⊢ ((((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉)) → if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
24 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) = (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
25 | 23, 24 | fmptd 6385 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) → (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ 𝑉)⟶Word ((mCN‘𝑇) ∪ 𝑉)) |
26 | | wrdco 13577 |
. . . . . . . 8
⊢ ((𝑒 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)):((mCN‘𝑇) ∪ 𝑉)⟶Word ((mCN‘𝑇) ∪ 𝑉)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒) ∈ Word Word ((mCN‘𝑇) ∪ 𝑉)) |
27 | 14, 25, 26 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) → ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒) ∈ Word Word ((mCN‘𝑇) ∪ 𝑉)) |
28 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘(freeMnd‘((mCN‘𝑇) ∪ 𝑉))) =
(Base‘(freeMnd‘((mCN‘𝑇) ∪ 𝑉))) |
29 | 6, 28 | frmdbas 17389 |
. . . . . . . . . 10
⊢
(((mCN‘𝑇)
∪ 𝑉) ∈ V →
(Base‘(freeMnd‘((mCN‘𝑇) ∪ 𝑉))) = Word ((mCN‘𝑇) ∪ 𝑉)) |
30 | 5, 29 | ax-mp 5 |
. . . . . . . . 9
⊢
(Base‘(freeMnd‘((mCN‘𝑇) ∪ 𝑉))) = Word ((mCN‘𝑇) ∪ 𝑉) |
31 | 30 | eqcomi 2631 |
. . . . . . . 8
⊢ Word
((mCN‘𝑇) ∪ 𝑉) =
(Base‘(freeMnd‘((mCN‘𝑇) ∪ 𝑉))) |
32 | 31 | gsumwcl 17377 |
. . . . . . 7
⊢
(((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) ∈ Mnd ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒) ∈ Word Word ((mCN‘𝑇) ∪ 𝑉)) → ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
33 | 8, 27, 32 | syl2anc 693 |
. . . . . 6
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) → ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
34 | 33, 13 | eleqtrrd 2704 |
. . . . 5
⊢ (((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑒 ∈ 𝑅) → ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) ∈ 𝑅) |
35 | | eqid 2622 |
. . . . 5
⊢ (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) |
36 | 34, 35 | fmptd 6385 |
. . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))):𝑅⟶𝑅) |
37 | | fvex 6201 |
. . . . . 6
⊢
(mREx‘𝑇)
∈ V |
38 | 11, 37 | eqeltri 2697 |
. . . . 5
⊢ 𝑅 ∈ V |
39 | 38, 38 | elmap 7886 |
. . . 4
⊢ ((𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) ∈ (𝑅 ↑𝑚 𝑅) ↔ (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))):𝑅⟶𝑅) |
40 | 36, 39 | sylibr 224 |
. . 3
⊢ ((𝑇 ∈ 𝑊 ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) ∈ (𝑅 ↑𝑚 𝑅)) |
41 | | eqid 2622 |
. . 3
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
42 | 40, 41 | fmptd 6385 |
. 2
⊢ (𝑇 ∈ 𝑊 → (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅)) |
43 | | mrsubvr.s |
. . . 4
⊢ 𝑆 = (mRSubst‘𝑇) |
44 | 10, 2, 11, 43, 6 | mrsubffval 31404 |
. . 3
⊢ (𝑇 ∈ 𝑊 → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))))) |
45 | 44 | feq1d 6030 |
. 2
⊢ (𝑇 ∈ 𝑊 → (𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅) ↔ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅))) |
46 | 42, 45 | mpbird 247 |
1
⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅)) |