Step | Hyp | Ref
| Expression |
1 | | msrfval.v |
. . . 4
⊢ 𝑉 = (mVars‘𝑇) |
2 | | msrfval.p |
. . . 4
⊢ 𝑃 = (mPreSt‘𝑇) |
3 | | msrfval.r |
. . . 4
⊢ 𝑅 = (mStRed‘𝑇) |
4 | 1, 2, 3 | msrfval 31712 |
. . 3
⊢ 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |
5 | 4 | a1i 11 |
. 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝑅 = (𝑠 ∈ 𝑃 ↦ ⦋(2nd
‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) |
6 | | fvexd 6352 |
. . 3
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) → (2nd
‘(1st ‘𝑠)) ∈ V) |
7 | | fvexd 6352 |
. . . 4
⊢
(((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) →
(2nd ‘𝑠)
∈ V) |
8 | | simpllr 817 |
. . . . . . . . 9
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝑠 = 〈𝐷, 𝐻, 𝐴〉) |
9 | 8 | fveq2d 6344 |
. . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘𝑠) = (1st
‘〈𝐷, 𝐻, 𝐴〉)) |
10 | 9 | fveq2d 6344 |
. . . . . . 7
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘(1st ‘𝑠)) = (1st ‘(1st
‘〈𝐷, 𝐻, 𝐴〉))) |
11 | | eqid 2748 |
. . . . . . . . . . . . 13
⊢
(mDV‘𝑇) =
(mDV‘𝑇) |
12 | | eqid 2748 |
. . . . . . . . . . . . 13
⊢
(mEx‘𝑇) =
(mEx‘𝑇) |
13 | 11, 12, 2 | elmpst 31711 |
. . . . . . . . . . . 12
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ↔ ((𝐷 ⊆ (mDV‘𝑇) ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇))) |
14 | 13 | simp1bi 1137 |
. . . . . . . . . . 11
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐷 ⊆ (mDV‘𝑇) ∧ ◡𝐷 = 𝐷)) |
15 | 14 | simpld 477 |
. . . . . . . . . 10
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝐷 ⊆ (mDV‘𝑇)) |
16 | 15 | ad3antrrr 768 |
. . . . . . . . 9
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐷 ⊆ (mDV‘𝑇)) |
17 | | fvex 6350 |
. . . . . . . . . 10
⊢
(mDV‘𝑇) ∈
V |
18 | 17 | ssex 4942 |
. . . . . . . . 9
⊢ (𝐷 ⊆ (mDV‘𝑇) → 𝐷 ∈ V) |
19 | 16, 18 | syl 17 |
. . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐷 ∈ V) |
20 | 13 | simp2bi 1138 |
. . . . . . . . . 10
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin)) |
21 | 20 | simprd 482 |
. . . . . . . . 9
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝐻 ∈ Fin) |
22 | 21 | ad3antrrr 768 |
. . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐻 ∈ Fin) |
23 | 13 | simp3bi 1139 |
. . . . . . . . 9
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 𝐴 ∈ (mEx‘𝑇)) |
24 | 23 | ad3antrrr 768 |
. . . . . . . 8
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝐴 ∈ (mEx‘𝑇)) |
25 | | ot1stg 7335 |
. . . . . . . 8
⊢ ((𝐷 ∈ V ∧ 𝐻 ∈ Fin ∧ 𝐴 ∈ (mEx‘𝑇)) → (1st
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐷) |
26 | 19, 22, 24, 25 | syl3anc 1463 |
. . . . . . 7
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐷) |
27 | 10, 26 | eqtrd 2782 |
. . . . . 6
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (1st
‘(1st ‘𝑠)) = 𝐷) |
28 | | fvex 6350 |
. . . . . . . . . . 11
⊢
(mVars‘𝑇)
∈ V |
29 | 1, 28 | eqeltri 2823 |
. . . . . . . . . 10
⊢ 𝑉 ∈ V |
30 | | imaexg 7256 |
. . . . . . . . . 10
⊢ (𝑉 ∈ V → (𝑉 “ (ℎ ∪ {𝑎})) ∈ V) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑉 “ (ℎ ∪ {𝑎})) ∈ V |
32 | 31 | uniex 7106 |
. . . . . . . 8
⊢ ∪ (𝑉
“ (ℎ ∪ {𝑎})) ∈ V |
33 | 32 | a1i 11 |
. . . . . . 7
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ∪ (𝑉
“ (ℎ ∪ {𝑎})) ∈ V) |
34 | | id 22 |
. . . . . . . . 9
⊢ (𝑧 = ∪
(𝑉 “ (ℎ ∪ {𝑎})) → 𝑧 = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) |
35 | | simplr 809 |
. . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ℎ = (2nd ‘(1st
‘𝑠))) |
36 | 9 | fveq2d 6344 |
. . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘(1st ‘𝑠)) = (2nd ‘(1st
‘〈𝐷, 𝐻, 𝐴〉))) |
37 | | ot2ndg 7336 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ V ∧ 𝐻 ∈ Fin ∧ 𝐴 ∈ (mEx‘𝑇)) → (2nd
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐻) |
38 | 19, 22, 24, 37 | syl3anc 1463 |
. . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘(1st ‘〈𝐷, 𝐻, 𝐴〉)) = 𝐻) |
39 | 35, 36, 38 | 3eqtrd 2786 |
. . . . . . . . . . . . 13
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ℎ = 𝐻) |
40 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝑎 = (2nd ‘𝑠)) |
41 | 8 | fveq2d 6344 |
. . . . . . . . . . . . . . 15
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘𝑠) = (2nd
‘〈𝐷, 𝐻, 𝐴〉)) |
42 | | ot3rdg 7337 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (mEx‘𝑇) → (2nd
‘〈𝐷, 𝐻, 𝐴〉) = 𝐴) |
43 | 24, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (2nd
‘〈𝐷, 𝐻, 𝐴〉) = 𝐴) |
44 | 40, 41, 43 | 3eqtrd 2786 |
. . . . . . . . . . . . . 14
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 𝑎 = 𝐴) |
45 | 44 | sneqd 4321 |
. . . . . . . . . . . . 13
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → {𝑎} = {𝐴}) |
46 | 39, 45 | uneq12d 3899 |
. . . . . . . . . . . 12
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (ℎ ∪ {𝑎}) = (𝐻 ∪ {𝐴})) |
47 | 46 | imaeq2d 5612 |
. . . . . . . . . . 11
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → (𝑉 “ (ℎ ∪ {𝑎})) = (𝑉 “ (𝐻 ∪ {𝐴}))) |
48 | 47 | unieqd 4586 |
. . . . . . . . . 10
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ∪ (𝑉
“ (ℎ ∪ {𝑎})) = ∪ (𝑉
“ (𝐻 ∪ {𝐴}))) |
49 | | msrval.z |
. . . . . . . . . 10
⊢ 𝑍 = ∪
(𝑉 “ (𝐻 ∪ {𝐴})) |
50 | 48, 49 | syl6eqr 2800 |
. . . . . . . . 9
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ∪ (𝑉
“ (ℎ ∪ {𝑎})) = 𝑍) |
51 | 34, 50 | sylan9eqr 2804 |
. . . . . . . 8
⊢
(((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) ∧ 𝑧 = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) → 𝑧 = 𝑍) |
52 | 51 | sqxpeqd 5286 |
. . . . . . 7
⊢
(((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) ∧ 𝑧 = ∪ (𝑉 “ (ℎ ∪ {𝑎}))) → (𝑧 × 𝑧) = (𝑍 × 𝑍)) |
53 | 33, 52 | csbied 3689 |
. . . . . 6
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧) = (𝑍 × 𝑍)) |
54 | 27, 53 | ineq12d 3946 |
. . . . 5
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → ((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)) = (𝐷 ∩ (𝑍 × 𝑍))) |
55 | 54, 39, 44 | oteq123d 4556 |
. . . 4
⊢
((((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) ∧ 𝑎 = (2nd ‘𝑠)) → 〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
56 | 7, 55 | csbied 3689 |
. . 3
⊢
(((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) ∧ ℎ = (2nd ‘(1st
‘𝑠))) →
⦋(2nd ‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
57 | 6, 56 | csbied 3689 |
. 2
⊢
((〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ∧ 𝑠 = 〈𝐷, 𝐻, 𝐴〉) →
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ (𝑉
“ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
58 | | id 22 |
. 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃) |
59 | | otex 5070 |
. . 3
⊢
〈(𝐷 ∩
(𝑍 × 𝑍)), 𝐻, 𝐴〉 ∈ V |
60 | 59 | a1i 11 |
. 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉 ∈ V) |
61 | 5, 57, 58, 60 | fvmptd 6438 |
1
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 → (𝑅‘〈𝐷, 𝐻, 𝐴〉) = 〈(𝐷 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |