Step | Hyp | Ref
| Expression |
1 | | mrsubffval.c |
. . . . . 6
⊢ 𝐶 = (mCN‘𝑇) |
2 | | mrsubffval.v |
. . . . . 6
⊢ 𝑉 = (mVR‘𝑇) |
3 | | mrsubffval.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
4 | | mrsubffval.s |
. . . . . 6
⊢ 𝑆 = (mRSubst‘𝑇) |
5 | | mrsubffval.g |
. . . . . 6
⊢ 𝐺 = (freeMnd‘(𝐶 ∪ 𝑉)) |
6 | 1, 2, 3, 4, 5 | mrsubffval 31404 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))))) |
7 | 6 | adantr 481 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))))) |
8 | | dmeq 5324 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) |
9 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶𝑅 → dom 𝐹 = 𝐴) |
10 | 9 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → dom 𝐹 = 𝐴) |
11 | 8, 10 | sylan9eqr 2678 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → dom 𝑓 = 𝐴) |
12 | 11 | eleq2d 2687 |
. . . . . . . . 9
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → (𝑣 ∈ dom 𝑓 ↔ 𝑣 ∈ 𝐴)) |
13 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
14 | 13 | fveq1d 6193 |
. . . . . . . . 9
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → (𝑓‘𝑣) = (𝐹‘𝑣)) |
15 | 12, 14 | ifbieq1d 4109 |
. . . . . . . 8
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉) = if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) |
16 | 15 | mpteq2dv 4745 |
. . . . . . 7
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉))) |
17 | 16 | coeq1d 5283 |
. . . . . 6
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒) = ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) |
18 | 17 | oveq2d 6666 |
. . . . 5
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) = (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) |
19 | 18 | mpteq2dv 4745 |
. . . 4
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) = (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
20 | | fvex 6201 |
. . . . . . 7
⊢
(mREx‘𝑇)
∈ V |
21 | 3, 20 | eqeltri 2697 |
. . . . . 6
⊢ 𝑅 ∈ V |
22 | 21 | a1i 11 |
. . . . 5
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝑅 ∈ V) |
23 | | fvex 6201 |
. . . . . . 7
⊢
(mVR‘𝑇) ∈
V |
24 | 2, 23 | eqeltri 2697 |
. . . . . 6
⊢ 𝑉 ∈ V |
25 | 24 | a1i 11 |
. . . . 5
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝑉 ∈ V) |
26 | | simprl 794 |
. . . . 5
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐹:𝐴⟶𝑅) |
27 | | simprr 796 |
. . . . 5
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐴 ⊆ 𝑉) |
28 | | elpm2r 7875 |
. . . . 5
⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐹 ∈ (𝑅 ↑pm 𝑉)) |
29 | 22, 25, 26, 27, 28 | syl22anc 1327 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐹 ∈ (𝑅 ↑pm 𝑉)) |
30 | 21 | mptex 6486 |
. . . . 5
⊢ (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) ∈ V |
31 | 30 | a1i 11 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) ∈ V) |
32 | 7, 19, 29, 31 | fvmptd 6288 |
. . 3
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → (𝑆‘𝐹) = (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
33 | 32 | ex 450 |
. 2
⊢ (𝑇 ∈ V → ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))))) |
34 | | 0fv 6227 |
. . . 4
⊢
(∅‘𝐹) =
∅ |
35 | | fvprc 6185 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mRSubst‘𝑇) =
∅) |
36 | 4, 35 | syl5eq 2668 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
37 | 36 | fveq1d 6193 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑆‘𝐹) = (∅‘𝐹)) |
38 | | fvprc 6185 |
. . . . . . 7
⊢ (¬
𝑇 ∈ V →
(mREx‘𝑇) =
∅) |
39 | 3, 38 | syl5eq 2668 |
. . . . . 6
⊢ (¬
𝑇 ∈ V → 𝑅 = ∅) |
40 | 39 | mpteq1d 4738 |
. . . . 5
⊢ (¬
𝑇 ∈ V → (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) = (𝑒 ∈ ∅ ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
41 | | mpt0 6021 |
. . . . 5
⊢ (𝑒 ∈ ∅ ↦ (𝐺 Σg
((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) = ∅ |
42 | 40, 41 | syl6eq 2672 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) = ∅) |
43 | 34, 37, 42 | 3eqtr4a 2682 |
. . 3
⊢ (¬
𝑇 ∈ V → (𝑆‘𝐹) = (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
44 | 43 | a1d 25 |
. 2
⊢ (¬
𝑇 ∈ V → ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))))) |
45 | 33, 44 | pm2.61i 176 |
1
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |