Step | Hyp | Ref
| Expression |
1 | | msrfval.v |
. . . 4
⊢ 𝑉 = (mVars‘𝑇) |
2 | | msrfval.p |
. . . 4
⊢ 𝑃 = (mPreSt‘𝑇) |
3 | | msrfval.r |
. . . 4
⊢ 𝑅 = (mStRed‘𝑇) |
4 | 1, 2, 3 | msrfval 30688 |
. . 3
⊢ 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |
5 | 4 | a1i 11 |
. 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) |
6 | | fvex 6113 |
. . . 4
⊢
(2nd ‘(1st ‘𝑠)) ∈ V |
7 | 6 | a1i 11 |
. . 3
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) → (2nd
‘(1st ‘𝑠)) ∈ V) |
8 | | fvex 6113 |
. . . . 5
⊢
(2nd ‘𝑠) ∈ V |
9 | 8 | a1i 11 |
. . . 4
⊢
(((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) →
(2nd ‘𝑠)
∈ V) |
10 | | simpllr 795 |
. . . . . . . . 9
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝑠 = 〈𝐷, 𝐻, 𝐴〉) |
11 | 10 | fveq2d 6107 |
. . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘𝑠) = (1st
‘〈𝐷, 𝐻, 𝐴〉)) |
12 | 11 | fveq2d 6107 |
. . . . . . 7
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘(1st ‘𝑠)) = (1st ‘(1st
‘〈𝐷, 𝐻, 𝐴〉))) |
13 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(mDV‘𝑇) =
(mDV‘𝑇) |
14 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(mEx‘𝑇) =
(mEx‘𝑇) |
15 | 13, 14, 2 | elmpst 30687 |
. . . . . . . . . . . 12
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ↔ ((𝐷 ⊆ (mDV‘𝑇) ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇))) |
16 | 15 | simp1bi 1069 |
. . . . . . . . . . 11
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐷 ⊆ (mDV‘𝑇) ∧ ◡𝐷 = 𝐷)) |
17 | 16 | simpld 474 |
. . . . . . . . . 10
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝐷 ⊆ (mDV‘𝑇)) |
18 | 17 | ad3antrrr 762 |
. . . . . . . . 9
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐷 ⊆ (mDV‘𝑇)) |
19 | | fvex 6113 |
. . . . . . . . . 10
⊢
(mDV‘𝑇) ∈
V |
20 | 19 | ssex 4730 |
. . . . . . . . 9
⊢ (𝐷 ⊆ (mDV‘𝑇) → 𝐷 ∈ V) |
21 | 18, 20 | syl 17 |
. . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐷 ∈ V) |
22 | 15 | simp2bi 1070 |
. . . . . . . . . 10
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin)) |
23 | 22 | simprd 478 |
. . . . . . . . 9
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝐻 ∈ Fin) |
24 | 23 | ad3antrrr 762 |
. . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐻 ∈ Fin) |
25 | 15 | simp3bi 1071 |
. . . . . . . . 9
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝐴 ∈ (mEx‘𝑇)) |
26 | 25 | ad3antrrr 762 |
. . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐴 ∈ (mEx‘𝑇)) |
27 | | ot1stg 7073 |
. . . . . . . 8
⊢ ((𝐷 ∈ V ∧ 𝐻 ∈ Fin ∧ 𝐴 ∈ (mEx‘𝑇)) → (1st
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐷) |
28 | 21, 24, 26, 27 | syl3anc 1318 |
. . . . . . 7
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐷) |
29 | 12, 28 | eqtrd 2644 |
. . . . . 6
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘(1st ‘𝑠)) = 𝐷) |
30 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(mVars‘𝑇)
∈ V |
31 | 1, 30 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝑉 ∈ V |
32 | | imaexg 6995 |
. . . . . . . . . 10
⊢ (𝑉 ∈ V → (𝑉 “ (ℎ ∪ {𝑎})) ∈ V) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑉 “ (ℎ ∪ {𝑎})) ∈ V |
34 | 33 | uniex 6851 |
. . . . . . . 8
⊢ ∪ (𝑉
“ (ℎ ∪ {𝑎})) ∈ V |
35 | 34 | a1i 11 |
. . . . . . 7
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ∪ (𝑉
“ (ℎ ∪ {𝑎})) ∈ V) |
36 | | id 22 |
. . . . . . . . 9
⊢ (𝑧 = ∪
(𝑉 “ (ℎ ∪ {𝑎})) → 𝑧 = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) |
37 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ℎ = (2nd ‘(1st
‘𝑠))) |
38 | 11 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘(1st ‘𝑠)) = (2nd ‘(1st
‘〈𝐷, 𝐻, 𝐴〉))) |
39 | | ot2ndg 7074 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ V ∧ 𝐻 ∈ Fin ∧ 𝐴 ∈ (mEx‘𝑇)) → (2nd
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐻) |
40 | 21, 24, 26, 39 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐻) |
41 | 37, 38, 40 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ℎ = 𝐻) |
42 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝑎 = (2nd ‘𝑠)) |
43 | 10 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘𝑠) = (2nd
‘〈𝐷, 𝐻, 𝐴〉)) |
44 | | ot3rdg 7075 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (mEx‘𝑇) → (2nd
‘〈𝐷, 𝐻, 𝐴〉) = 𝐴) |
45 | 26, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘〈𝐷, 𝐻, 𝐴〉) = 𝐴) |
46 | 42, 43, 45 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝑎 = 𝐴) |
47 | 46 | sneqd 4137 |
. . . . . . . . . . . . 13
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → {𝑎} = {𝐴}) |
48 | 41, 47 | uneq12d 3730 |
. . . . . . . . . . . 12
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (ℎ ∪ {𝑎}) = (𝐻 ∪ {𝐴})) |
49 | 48 | imaeq2d 5385 |
. . . . . . . . . . 11
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (𝑉 “ (ℎ ∪ {𝑎})) = (𝑉 “ (𝐻 ∪ {𝐴}))) |
50 | 49 | unieqd 4382 |
. . . . . . . . . 10
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ∪ (𝑉
“ (ℎ ∪ {𝑎})) = ∪ (𝑉
“ (𝐻 ∪ {𝐴}))) |
51 | | msrval.z |
. . . . . . . . . 10
⊢ 𝑍 = ∪
(𝑉 “ (𝐻 ∪ {𝐴})) |
52 | 50, 51 | syl6eqr 2662 |
. . . . . . . . 9
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ∪ (𝑉
“ (ℎ ∪ {𝑎})) = 𝑍) |
53 | 36, 52 | sylan9eqr 2666 |
. . . . . . . 8
⊢
(((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) ∧ 𝑧 = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) → 𝑧 = 𝑍) |
54 | 53 | sqxpeqd 5065 |
. . . . . . 7
⊢
(((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) ∧ 𝑧 = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) → (𝑧 × 𝑧) = (𝑍 × 𝑍)) |
55 | 35, 54 | csbied 3526 |
. . . . . 6
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧) = (𝑍 × 𝑍)) |
56 | 29, 55 | ineq12d 3777 |
. . . . 5
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)) = (𝐷 ∩ (𝑍 × 𝑍))) |
57 | 56, 41, 46 | oteq123d 4355 |
. . . 4
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
58 | 9, 57 | csbied 3526 |
. . 3
⊢
(((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) →
⦋(2nd ‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
59 | 7, 58 | csbied 3526 |
. 2
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) →
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
60 | | id 22 |
. 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃) |
61 | | otex 4860 |
. . 3
⊢
〈(𝐷 ∩
(𝑍 × 𝑍)), 𝐻, 𝐴〉 ∈ V |
62 | 61 | a1i 11 |
. 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉 ∈ V) |
63 | 5, 59, 60, 62 | fvmptd 6197 |
1
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝑅‘〈𝐷, 𝐻, 𝐴〉) = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |