| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | msrfval.r | . 2
⊢ 𝑅 = (mStRed‘𝑇) | 
| 2 |  | fveq2 6906 | . . . . . 6
⊢ (𝑡 = 𝑇 → (mPreSt‘𝑡) = (mPreSt‘𝑇)) | 
| 3 |  | msrfval.p | . . . . . 6
⊢ 𝑃 = (mPreSt‘𝑇) | 
| 4 | 2, 3 | eqtr4di 2795 | . . . . 5
⊢ (𝑡 = 𝑇 → (mPreSt‘𝑡) = 𝑃) | 
| 5 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → (mVars‘𝑡) = (mVars‘𝑇)) | 
| 6 |  | msrfval.v | . . . . . . . . . . . . 13
⊢ 𝑉 = (mVars‘𝑇) | 
| 7 | 5, 6 | eqtr4di 2795 | . . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (mVars‘𝑡) = 𝑉) | 
| 8 | 7 | imaeq1d 6077 | . . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) = (𝑉 “ (ℎ ∪ {𝑎}))) | 
| 9 | 8 | unieqd 4920 | . . . . . . . . . 10
⊢ (𝑡 = 𝑇 → ∪
((mVars‘𝑡) “
(ℎ ∪ {𝑎})) = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) | 
| 10 | 9 | csbeq1d 3903 | . . . . . . . . 9
⊢ (𝑡 = 𝑇 → ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧) = ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)) | 
| 11 | 10 | ineq2d 4220 | . . . . . . . 8
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)) = ((1st ‘(1st
‘𝑠)) ∩
⦋∪ (𝑉 “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧))) | 
| 12 | 11 | oteq1d 4885 | . . . . . . 7
⊢ (𝑡 = 𝑇 → 〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) | 
| 13 | 12 | csbeq2dv 3906 | . . . . . 6
⊢ (𝑡 = 𝑇 → ⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = ⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) | 
| 14 | 13 | csbeq2dv 3906 | . . . . 5
⊢ (𝑡 = 𝑇 → ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) | 
| 15 | 4, 14 | mpteq12dv 5233 | . . . 4
⊢ (𝑡 = 𝑇 → (𝑠 ∈ (mPreSt‘𝑡) ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) | 
| 16 |  | df-msr 35499 | . . . 4
⊢ mStRed =
(𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) | 
| 17 | 15, 16, 3 | mptfvmpt 7248 | . . 3
⊢ (𝑇 ∈ V →
(mStRed‘𝑇) = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) | 
| 18 |  | mpt0 6710 | . . . . 5
⊢ (𝑠 ∈ ∅ ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) = ∅ | 
| 19 | 18 | eqcomi 2746 | . . . 4
⊢ ∅ =
(𝑠 ∈ ∅ ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) | 
| 20 |  | fvprc 6898 | . . . 4
⊢ (¬
𝑇 ∈ V →
(mStRed‘𝑇) =
∅) | 
| 21 |  | fvprc 6898 | . . . . . 6
⊢ (¬
𝑇 ∈ V →
(mPreSt‘𝑇) =
∅) | 
| 22 | 3, 21 | eqtrid 2789 | . . . . 5
⊢ (¬
𝑇 ∈ V → 𝑃 = ∅) | 
| 23 | 22 | mpteq1d 5237 | . . . 4
⊢ (¬
𝑇 ∈ V → (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) = (𝑠 ∈ ∅ ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) | 
| 24 | 19, 20, 23 | 3eqtr4a 2803 | . . 3
⊢ (¬
𝑇 ∈ V →
(mStRed‘𝑇) = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) | 
| 25 | 17, 24 | pm2.61i 182 | . 2
⊢
(mStRed‘𝑇) =
(𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) | 
| 26 | 1, 25 | eqtri 2765 | 1
⊢ 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |