| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | msrfval.v | . . . 4
⊢ 𝑉 = (mVars‘𝑇) | 
| 2 |  | msrfval.p | . . . 4
⊢ 𝑃 = (mPreSt‘𝑇) | 
| 3 |  | msrfval.r | . . . 4
⊢ 𝑅 = (mStRed‘𝑇) | 
| 4 | 1, 2, 3 | msrfval 35542 | . . 3
⊢ 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) | 
| 5 | 4 | a1i 11 | . 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) | 
| 6 |  | fvexd 6921 | . . 3
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) → (2nd
‘(1st ‘𝑠)) ∈ V) | 
| 7 |  | fvexd 6921 | . . . 4
⊢
(((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) →
(2nd ‘𝑠)
∈ V) | 
| 8 |  | simpllr 776 | . . . . . . . . 9
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝑠 = 〈𝐷, 𝐻, 𝐴〉) | 
| 9 | 8 | fveq2d 6910 | . . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘𝑠) = (1st
‘〈𝐷, 𝐻, 𝐴〉)) | 
| 10 | 9 | fveq2d 6910 | . . . . . . 7
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘(1st ‘𝑠)) = (1st ‘(1st
‘〈𝐷, 𝐻, 𝐴〉))) | 
| 11 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(mDV‘𝑇) =
(mDV‘𝑇) | 
| 12 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(mEx‘𝑇) =
(mEx‘𝑇) | 
| 13 | 11, 12, 2 | elmpst 35541 | . . . . . . . . . . . 12
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ↔ ((𝐷 ⊆ (mDV‘𝑇) ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇))) | 
| 14 | 13 | simp1bi 1146 | . . . . . . . . . . 11
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐷 ⊆ (mDV‘𝑇) ∧ ◡𝐷 = 𝐷)) | 
| 15 | 14 | simpld 494 | . . . . . . . . . 10
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝐷 ⊆ (mDV‘𝑇)) | 
| 16 | 15 | ad3antrrr 730 | . . . . . . . . 9
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐷 ⊆ (mDV‘𝑇)) | 
| 17 |  | fvex 6919 | . . . . . . . . . 10
⊢
(mDV‘𝑇) ∈
V | 
| 18 | 17 | ssex 5321 | . . . . . . . . 9
⊢ (𝐷 ⊆ (mDV‘𝑇) → 𝐷 ∈ V) | 
| 19 | 16, 18 | syl 17 | . . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐷 ∈ V) | 
| 20 | 13 | simp2bi 1147 | . . . . . . . . . 10
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin)) | 
| 21 | 20 | simprd 495 | . . . . . . . . 9
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝐻 ∈ Fin) | 
| 22 | 21 | ad3antrrr 730 | . . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐻 ∈ Fin) | 
| 23 | 13 | simp3bi 1148 | . . . . . . . . 9
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝐴 ∈ (mEx‘𝑇)) | 
| 24 | 23 | ad3antrrr 730 | . . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐴 ∈ (mEx‘𝑇)) | 
| 25 |  | ot1stg 8028 | . . . . . . . 8
⊢ ((𝐷 ∈ V ∧ 𝐻 ∈ Fin ∧ 𝐴 ∈ (mEx‘𝑇)) → (1st
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐷) | 
| 26 | 19, 22, 24, 25 | syl3anc 1373 | . . . . . . 7
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐷) | 
| 27 | 10, 26 | eqtrd 2777 | . . . . . 6
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘(1st ‘𝑠)) = 𝐷) | 
| 28 | 1 | fvexi 6920 | . . . . . . . . . 10
⊢ 𝑉 ∈ V | 
| 29 |  | imaexg 7935 | . . . . . . . . . 10
⊢ (𝑉 ∈ V → (𝑉 “ (ℎ ∪ {𝑎})) ∈ V) | 
| 30 | 28, 29 | ax-mp 5 | . . . . . . . . 9
⊢ (𝑉 “ (ℎ ∪ {𝑎})) ∈ V | 
| 31 | 30 | uniex 7761 | . . . . . . . 8
⊢ ∪ (𝑉
“ (ℎ ∪ {𝑎})) ∈ V | 
| 32 | 31 | a1i 11 | . . . . . . 7
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ∪ (𝑉
“ (ℎ ∪ {𝑎})) ∈ V) | 
| 33 |  | id 22 | . . . . . . . . 9
⊢ (𝑧 = ∪
(𝑉 “ (ℎ ∪ {𝑎})) → 𝑧 = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) | 
| 34 |  | simplr 769 | . . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ℎ = (2nd ‘(1st
‘𝑠))) | 
| 35 | 9 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘(1st ‘𝑠)) = (2nd ‘(1st
‘〈𝐷, 𝐻, 𝐴〉))) | 
| 36 |  | ot2ndg 8029 | . . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ V ∧ 𝐻 ∈ Fin ∧ 𝐴 ∈ (mEx‘𝑇)) → (2nd
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐻) | 
| 37 | 19, 22, 24, 36 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐻) | 
| 38 | 34, 35, 37 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ℎ = 𝐻) | 
| 39 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝑎 = (2nd ‘𝑠)) | 
| 40 | 8 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘𝑠) = (2nd
‘〈𝐷, 𝐻, 𝐴〉)) | 
| 41 |  | ot3rdg 8030 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (mEx‘𝑇) → (2nd
‘〈𝐷, 𝐻, 𝐴〉) = 𝐴) | 
| 42 | 24, 41 | syl 17 | . . . . . . . . . . . . . . 15
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘〈𝐷, 𝐻, 𝐴〉) = 𝐴) | 
| 43 | 39, 40, 42 | 3eqtrd 2781 | . . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝑎 = 𝐴) | 
| 44 | 43 | sneqd 4638 | . . . . . . . . . . . . 13
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → {𝑎} = {𝐴}) | 
| 45 | 38, 44 | uneq12d 4169 | . . . . . . . . . . . 12
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (ℎ ∪ {𝑎}) = (𝐻 ∪ {𝐴})) | 
| 46 | 45 | imaeq2d 6078 | . . . . . . . . . . 11
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (𝑉 “ (ℎ ∪ {𝑎})) = (𝑉 “ (𝐻 ∪ {𝐴}))) | 
| 47 | 46 | unieqd 4920 | . . . . . . . . . 10
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ∪ (𝑉
“ (ℎ ∪ {𝑎})) = ∪ (𝑉
“ (𝐻 ∪ {𝐴}))) | 
| 48 |  | msrval.z | . . . . . . . . . 10
⊢ 𝑍 = ∪
(𝑉 “ (𝐻 ∪ {𝐴})) | 
| 49 | 47, 48 | eqtr4di 2795 | . . . . . . . . 9
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ∪ (𝑉
“ (ℎ ∪ {𝑎})) = 𝑍) | 
| 50 | 33, 49 | sylan9eqr 2799 | . . . . . . . 8
⊢
(((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) ∧ 𝑧 = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) → 𝑧 = 𝑍) | 
| 51 | 50 | sqxpeqd 5717 | . . . . . . 7
⊢
(((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) ∧ 𝑧 = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) → (𝑧 × 𝑧) = (𝑍 × 𝑍)) | 
| 52 | 32, 51 | csbied 3935 | . . . . . 6
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧) = (𝑍 × 𝑍)) | 
| 53 | 27, 52 | ineq12d 4221 | . . . . 5
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)) = (𝐷 ∩ (𝑍 × 𝑍))) | 
| 54 | 53, 38, 43 | oteq123d 4888 | . . . 4
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 55 | 7, 54 | csbied 3935 | . . 3
⊢
(((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) →
⦋(2nd ‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 56 | 6, 55 | csbied 3935 | . 2
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) →
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 57 |  | id 22 | . 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃) | 
| 58 |  | otex 5470 | . . 3
⊢
〈(𝐷 ∩
(𝑍 × 𝑍)), 𝐻, 𝐴〉 ∈ V | 
| 59 | 58 | a1i 11 | . 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉 ∈ V) | 
| 60 | 5, 56, 57, 59 | fvmptd 7023 | 1
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝑅‘〈𝐷, 𝐻, 𝐴〉) = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |