Step | Hyp | Ref
| Expression |
1 | | mrsubvr.v |
. . . . . . 7
⊢ 𝑉 = (mVR‘𝑇) |
2 | | mrsubvr.r |
. . . . . . 7
⊢ 𝑅 = (mREx‘𝑇) |
3 | | mrsubvr.s |
. . . . . . 7
⊢ 𝑆 = (mRSubst‘𝑇) |
4 | 1, 2, 3 | mrsubff 30663 |
. . . . . 6
⊢ (𝑇 ∈ V → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅)) |
5 | | ffn 5958 |
. . . . . 6
⊢ (𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
7 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑣 → (𝑥 ∈ dom 𝑓 ↔ 𝑣 ∈ dom 𝑓)) |
8 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑣 → (𝑓‘𝑥) = (𝑓‘𝑣)) |
9 | | s1eq 13233 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑣 → 〈“𝑥”〉 = 〈“𝑣”〉) |
10 | 7, 8, 9 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑣 → if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉) = if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
11 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) = (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) |
12 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓‘𝑣) ∈ V |
13 | | s1cli 13237 |
. . . . . . . . . . . . . . . . . . 19
⊢
〈“𝑣”〉 ∈ Word V |
14 | 13 | elexi 3186 |
. . . . . . . . . . . . . . . . . 18
⊢
〈“𝑣”〉 ∈ V |
15 | 12, 14 | ifex 4106 |
. . . . . . . . . . . . . . . . 17
⊢ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉) ∈ V |
16 | 10, 11, 15 | fvmpt 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ 𝑉 → ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣) = if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑣 ∈ 𝑉) → ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣) = if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
18 | 17 | ifeq1da 4066 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉) = if(𝑣 ∈ 𝑉, if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉), 〈“𝑣”〉)) |
19 | | ifan 4084 |
. . . . . . . . . . . . . 14
⊢ if((𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓), (𝑓‘𝑣), 〈“𝑣”〉) = if(𝑣 ∈ 𝑉, if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉), 〈“𝑣”〉) |
20 | 18, 19 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉) = if((𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓), (𝑓‘𝑣), 〈“𝑣”〉)) |
21 | | elpmi 7762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) → (𝑓:dom 𝑓⟶𝑅 ∧ dom 𝑓 ⊆ 𝑉)) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑓:dom 𝑓⟶𝑅 ∧ dom 𝑓 ⊆ 𝑉)) |
23 | 22 | simprd 478 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → dom 𝑓 ⊆ 𝑉) |
24 | 23 | sseld 3567 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑣 ∈ dom 𝑓 → 𝑣 ∈ 𝑉)) |
25 | 24 | pm4.71rd 665 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑣 ∈ dom 𝑓 ↔ (𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓))) |
26 | 25 | bicomd 212 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓) ↔ 𝑣 ∈ dom 𝑓)) |
27 | 26 | ifbid 4058 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → if((𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓), (𝑓‘𝑣), 〈“𝑣”〉) = if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
28 | 20, 27 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉) = if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) |
29 | 28 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) = (𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉))) |
30 | 29 | coeq1d 5205 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒) = ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) |
31 | 30 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) →
((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) = ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) |
32 | 31 | mpteq2dv 4673 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
33 | | eqid 2610 |
. . . . . . . . . 10
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
34 | | eqid 2610 |
. . . . . . . . . 10
⊢
(freeMnd‘((mCN‘𝑇) ∪ 𝑉)) = (freeMnd‘((mCN‘𝑇) ∪ 𝑉)) |
35 | 33, 1, 2, 3, 34 | mrsubfval 30659 |
. . . . . . . . 9
⊢ ((𝑓:dom 𝑓⟶𝑅 ∧ dom 𝑓 ⊆ 𝑉) → (𝑆‘𝑓) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
36 | 22, 35 | syl 17 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘𝑓) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
37 | 22 | simpld 474 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → 𝑓:dom 𝑓⟶𝑅) |
38 | 37 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) → 𝑓:dom 𝑓⟶𝑅) |
39 | 38 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ 𝑅) |
40 | | elun2 3743 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∈ ((mCN‘𝑇) ∪ 𝑉)) |
41 | 40 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 𝑥 ∈ ((mCN‘𝑇) ∪ 𝑉)) |
42 | 41 | s1cld 13236 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 〈“𝑥”〉 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
43 | 33, 1, 2 | mrexval 30652 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
44 | 43 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
45 | 42, 44 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 ∈ dom 𝑓) → 〈“𝑥”〉 ∈ 𝑅) |
46 | 39, 45 | ifclda 4070 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑥 ∈ 𝑉) → if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉) ∈ 𝑅) |
47 | 46, 11 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)):𝑉⟶𝑅) |
48 | | ssid 3587 |
. . . . . . . . 9
⊢ 𝑉 ⊆ 𝑉 |
49 | 33, 1, 2, 3, 34 | mrsubfval 30659 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)):𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
50 | 47, 48, 49 | sylancl 693 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))) = (𝑒 ∈ 𝑅 ↦ ((freeMnd‘((mCN‘𝑇) ∪ 𝑉)) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ 𝑉) ↦ if(𝑣 ∈ 𝑉, ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
51 | 32, 36, 50 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘𝑓) = (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)))) |
52 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
53 | | mapsspm 7777 |
. . . . . . . . 9
⊢ (𝑅 ↑𝑚
𝑉) ⊆ (𝑅 ↑pm
𝑉) |
54 | 53 | a1i 11 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑅 ↑𝑚 𝑉) ⊆ (𝑅 ↑pm 𝑉)) |
55 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(mREx‘𝑇)
∈ V |
56 | 2, 55 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝑅 ∈ V |
57 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(mVR‘𝑇) ∈
V |
58 | 1, 57 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝑉 ∈ V |
59 | 56, 58 | elmap 7772 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) ∈ (𝑅 ↑𝑚 𝑉) ↔ (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)):𝑉⟶𝑅) |
60 | 47, 59 | sylibr 223 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) ∈ (𝑅 ↑𝑚 𝑉)) |
61 | | fnfvima 6400 |
. . . . . . . 8
⊢ ((𝑆 Fn (𝑅 ↑pm 𝑉) ∧ (𝑅 ↑𝑚 𝑉) ⊆ (𝑅 ↑pm 𝑉) ∧ (𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉)) ∈ (𝑅 ↑𝑚 𝑉)) → (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
62 | 52, 54, 60, 61 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘(𝑥 ∈ 𝑉 ↦ if(𝑥 ∈ dom 𝑓, (𝑓‘𝑥), 〈“𝑥”〉))) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
63 | 51, 62 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑆‘𝑓) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
64 | 63 | ralrimiva 2949 |
. . . . 5
⊢ (𝑇 ∈ V → ∀𝑓 ∈ (𝑅 ↑pm 𝑉)(𝑆‘𝑓) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
65 | | ffnfv 6295 |
. . . . 5
⊢ (𝑆:(𝑅 ↑pm 𝑉)⟶(𝑆 “ (𝑅 ↑𝑚 𝑉)) ↔ (𝑆 Fn (𝑅 ↑pm 𝑉) ∧ ∀𝑓 ∈ (𝑅 ↑pm 𝑉)(𝑆‘𝑓) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉)))) |
66 | 6, 64, 65 | sylanbrc 695 |
. . . 4
⊢ (𝑇 ∈ V → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑆 “ (𝑅 ↑𝑚 𝑉))) |
67 | | frn 5966 |
. . . 4
⊢ (𝑆:(𝑅 ↑pm 𝑉)⟶(𝑆 “ (𝑅 ↑𝑚 𝑉)) → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
68 | 66, 67 | syl 17 |
. . 3
⊢ (𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
69 | | fvprc 6097 |
. . . . . . 7
⊢ (¬
𝑇 ∈ V →
(mRSubst‘𝑇) =
∅) |
70 | 3, 69 | syl5eq 2656 |
. . . . . 6
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
71 | 70 | rneqd 5274 |
. . . . 5
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ran ∅) |
72 | | rn0 5298 |
. . . . 5
⊢ ran
∅ = ∅ |
73 | 71, 72 | syl6eq 2660 |
. . . 4
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
74 | | 0ss 3924 |
. . . 4
⊢ ∅
⊆ (𝑆 “ (𝑅 ↑𝑚
𝑉)) |
75 | 73, 74 | syl6eqss 3618 |
. . 3
⊢ (¬
𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
76 | 68, 75 | pm2.61i 175 |
. 2
⊢ ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑𝑚 𝑉)) |
77 | | imassrn 5396 |
. 2
⊢ (𝑆 “ (𝑅 ↑𝑚 𝑉)) ⊆ ran 𝑆 |
78 | 76, 77 | eqssi 3584 |
1
⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑𝑚 𝑉)) |