Step | Hyp | Ref
| Expression |
1 | | msrfval.r |
. 2
⊢ 𝑅 = (mStRed‘𝑇) |
2 | | fveq2 6191 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (mPreSt‘𝑡) = (mPreSt‘𝑇)) |
3 | | msrfval.p |
. . . . . 6
⊢ 𝑃 = (mPreSt‘𝑇) |
4 | 2, 3 | syl6eqr 2674 |
. . . . 5
⊢ (𝑡 = 𝑇 → (mPreSt‘𝑡) = 𝑃) |
5 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → (mVars‘𝑡) = (mVars‘𝑇)) |
6 | | msrfval.v |
. . . . . . . . . . . . 13
⊢ 𝑉 = (mVars‘𝑇) |
7 | 5, 6 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (mVars‘𝑡) = 𝑉) |
8 | 7 | imaeq1d 5465 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) = (𝑉 “ (ℎ ∪ {𝑎}))) |
9 | 8 | unieqd 4446 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → ∪
((mVars‘𝑡) “
(ℎ ∪ {𝑎})) = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) |
10 | 9 | csbeq1d 3540 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧) = ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)) |
11 | 10 | ineq2d 3814 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)) = ((1st ‘(1st
‘𝑠)) ∩
⦋∪ (𝑉 “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧))) |
12 | 11 | oteq1d 4414 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → 〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |
13 | 12 | csbeq2dv 3992 |
. . . . . 6
⊢ (𝑡 = 𝑇 → ⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = ⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |
14 | 13 | csbeq2dv 3992 |
. . . . 5
⊢ (𝑡 = 𝑇 → ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |
15 | 4, 14 | mpteq12dv 4733 |
. . . 4
⊢ (𝑡 = 𝑇 → (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) |
16 | | df-msr 31391 |
. . . 4
⊢ mStRed =
(𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) |
17 | | fvex 6201 |
. . . . . 6
⊢
(mPreSt‘𝑇)
∈ V |
18 | 3, 17 | eqeltri 2697 |
. . . . 5
⊢ 𝑃 ∈ V |
19 | 18 | mptex 6486 |
. . . 4
⊢ (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) ∈ V |
20 | 15, 16, 19 | fvmpt 6282 |
. . 3
⊢ (𝑇 ∈ V →
(mStRed‘𝑇) = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) |
21 | | mpt0 6021 |
. . . . 5
⊢ (𝑠 ∈ ∅ ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) = ∅ |
22 | 21 | eqcomi 2631 |
. . . 4
⊢ ∅ =
(𝑠 ∈ ∅ ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |
23 | | fvprc 6185 |
. . . 4
⊢ (¬
𝑇 ∈ V →
(mStRed‘𝑇) =
∅) |
24 | | fvprc 6185 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mPreSt‘𝑇) =
∅) |
25 | 3, 24 | syl5eq 2668 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝑃 = ∅) |
26 | 25 | mpteq1d 4738 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) = (𝑠 ∈ ∅ ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) |
27 | 22, 23, 26 | 3eqtr4a 2682 |
. . 3
⊢ (¬
𝑇 ∈ V →
(mStRed‘𝑇) = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) |
28 | 20, 27 | pm2.61i 176 |
. 2
⊢
(mStRed‘𝑇) =
(𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |
29 | 1, 28 | eqtri 2644 |
1
⊢ 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |