Step | Hyp | Ref
| Expression |
1 | | msrfval.v |
. . . 4
β’ π = (mVarsβπ) |
2 | | msrfval.p |
. . . 4
β’ π = (mPreStβπ) |
3 | | msrfval.r |
. . . 4
β’ π
= (mStRedβπ) |
4 | 1, 2, 3 | msrfval 34195 |
. . 3
β’ π
= (π β π β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©) |
5 | 4 | a1i 11 |
. 2
β’
(β¨π·, π», π΄β© β π β π
= (π β π β¦ β¦(2nd
β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ©)) |
6 | | fvexd 6861 |
. . 3
β’
((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β (2nd
β(1st βπ )) β V) |
7 | | fvexd 6861 |
. . . 4
β’
(((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β
(2nd βπ )
β V) |
8 | | simpllr 775 |
. . . . . . . . 9
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β π = β¨π·, π», π΄β©) |
9 | 8 | fveq2d 6850 |
. . . . . . . 8
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (1st
βπ ) = (1st
ββ¨π·, π», π΄β©)) |
10 | 9 | fveq2d 6850 |
. . . . . . 7
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (1st
β(1st βπ )) = (1st β(1st
ββ¨π·, π», π΄β©))) |
11 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(mDVβπ) =
(mDVβπ) |
12 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(mExβπ) =
(mExβπ) |
13 | 11, 12, 2 | elmpst 34194 |
. . . . . . . . . . . 12
β’
(β¨π·, π», π΄β© β π β ((π· β (mDVβπ) β§ β‘π· = π·) β§ (π» β (mExβπ) β§ π» β Fin) β§ π΄ β (mExβπ))) |
14 | 13 | simp1bi 1146 |
. . . . . . . . . . 11
β’
(β¨π·, π», π΄β© β π β (π· β (mDVβπ) β§ β‘π· = π·)) |
15 | 14 | simpld 496 |
. . . . . . . . . 10
β’
(β¨π·, π», π΄β© β π β π· β (mDVβπ)) |
16 | 15 | ad3antrrr 729 |
. . . . . . . . 9
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β π· β (mDVβπ)) |
17 | | fvex 6859 |
. . . . . . . . . 10
β’
(mDVβπ) β
V |
18 | 17 | ssex 5282 |
. . . . . . . . 9
β’ (π· β (mDVβπ) β π· β V) |
19 | 16, 18 | syl 17 |
. . . . . . . 8
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β π· β V) |
20 | 13 | simp2bi 1147 |
. . . . . . . . . 10
β’
(β¨π·, π», π΄β© β π β (π» β (mExβπ) β§ π» β Fin)) |
21 | 20 | simprd 497 |
. . . . . . . . 9
β’
(β¨π·, π», π΄β© β π β π» β Fin) |
22 | 21 | ad3antrrr 729 |
. . . . . . . 8
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β π» β Fin) |
23 | 13 | simp3bi 1148 |
. . . . . . . . 9
β’
(β¨π·, π», π΄β© β π β π΄ β (mExβπ)) |
24 | 23 | ad3antrrr 729 |
. . . . . . . 8
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β π΄ β (mExβπ)) |
25 | | ot1stg 7939 |
. . . . . . . 8
β’ ((π· β V β§ π» β Fin β§ π΄ β (mExβπ)) β (1st
β(1st ββ¨π·, π», π΄β©)) = π·) |
26 | 19, 22, 24, 25 | syl3anc 1372 |
. . . . . . 7
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (1st
β(1st ββ¨π·, π», π΄β©)) = π·) |
27 | 10, 26 | eqtrd 2773 |
. . . . . 6
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (1st
β(1st βπ )) = π·) |
28 | 1 | fvexi 6860 |
. . . . . . . . . 10
β’ π β V |
29 | | imaexg 7856 |
. . . . . . . . . 10
β’ (π β V β (π β (β βͺ {π})) β V) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . 9
β’ (π β (β βͺ {π})) β V |
31 | 30 | uniex 7682 |
. . . . . . . 8
β’ βͺ (π
β (β βͺ {π})) β V |
32 | 31 | a1i 11 |
. . . . . . 7
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β βͺ (π
β (β βͺ {π})) β V) |
33 | | id 22 |
. . . . . . . . 9
β’ (π§ = βͺ
(π β (β βͺ {π})) β π§ = βͺ (π β (β βͺ {π}))) |
34 | | simplr 768 |
. . . . . . . . . . . . . 14
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β β = (2nd β(1st
βπ ))) |
35 | 9 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (2nd
β(1st βπ )) = (2nd β(1st
ββ¨π·, π», π΄β©))) |
36 | | ot2ndg 7940 |
. . . . . . . . . . . . . . 15
β’ ((π· β V β§ π» β Fin β§ π΄ β (mExβπ)) β (2nd
β(1st ββ¨π·, π», π΄β©)) = π») |
37 | 19, 22, 24, 36 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (2nd
β(1st ββ¨π·, π», π΄β©)) = π») |
38 | 34, 35, 37 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β β = π») |
39 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β π = (2nd βπ )) |
40 | 8 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (2nd
βπ ) = (2nd
ββ¨π·, π», π΄β©)) |
41 | | ot3rdg 7941 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (mExβπ) β (2nd
ββ¨π·, π», π΄β©) = π΄) |
42 | 24, 41 | syl 17 |
. . . . . . . . . . . . . . 15
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (2nd
ββ¨π·, π», π΄β©) = π΄) |
43 | 39, 40, 42 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β π = π΄) |
44 | 43 | sneqd 4602 |
. . . . . . . . . . . . 13
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β {π} = {π΄}) |
45 | 38, 44 | uneq12d 4128 |
. . . . . . . . . . . 12
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (β βͺ {π}) = (π» βͺ {π΄})) |
46 | 45 | imaeq2d 6017 |
. . . . . . . . . . 11
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β (π β (β βͺ {π})) = (π β (π» βͺ {π΄}))) |
47 | 46 | unieqd 4883 |
. . . . . . . . . 10
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β βͺ (π
β (β βͺ {π})) = βͺ (π
β (π» βͺ {π΄}))) |
48 | | msrval.z |
. . . . . . . . . 10
β’ π = βͺ
(π β (π» βͺ {π΄})) |
49 | 47, 48 | eqtr4di 2791 |
. . . . . . . . 9
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β βͺ (π
β (β βͺ {π})) = π) |
50 | 33, 49 | sylan9eqr 2795 |
. . . . . . . 8
β’
(((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β§ π§ = βͺ (π β (β βͺ {π}))) β π§ = π) |
51 | 50 | sqxpeqd 5669 |
. . . . . . 7
β’
(((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β§ π§ = βͺ (π β (β βͺ {π}))) β (π§ Γ π§) = (π Γ π)) |
52 | 32, 51 | csbied 3897 |
. . . . . 6
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§) = (π Γ π)) |
53 | 27, 52 | ineq12d 4177 |
. . . . 5
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β ((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)) = (π· β© (π Γ π))) |
54 | 53, 38, 43 | oteq123d 4849 |
. . . 4
β’
((((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β§ π = (2nd βπ )) β β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© = β¨(π· β© (π Γ π)), π», π΄β©) |
55 | 7, 54 | csbied 3897 |
. . 3
β’
(((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β§ β = (2nd β(1st
βπ ))) β
β¦(2nd βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© = β¨(π· β© (π Γ π)), π», π΄β©) |
56 | 6, 55 | csbied 3897 |
. 2
β’
((β¨π·, π», π΄β© β π β§ π = β¨π·, π», π΄β©) β
β¦(2nd β(1st βπ )) / ββ¦β¦(2nd
βπ ) / πβ¦β¨((1st
β(1st βπ )) β© β¦βͺ (π
β (β βͺ {π})) / π§β¦(π§ Γ π§)), β, πβ© = β¨(π· β© (π Γ π)), π», π΄β©) |
57 | | id 22 |
. 2
β’
(β¨π·, π», π΄β© β π β β¨π·, π», π΄β© β π) |
58 | | otex 5426 |
. . 3
β’
β¨(π· β©
(π Γ π)), π», π΄β© β V |
59 | 58 | a1i 11 |
. 2
β’
(β¨π·, π», π΄β© β π β β¨(π· β© (π Γ π)), π», π΄β© β V) |
60 | 5, 56, 57, 59 | fvmptd 6959 |
1
β’
(β¨π·, π», π΄β© β π β (π
ββ¨π·, π», π΄β©) = β¨(π· β© (π Γ π)), π», π΄β©) |