Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(mPreStβπ) =
(mPreStβπ) |
2 | | mstaval.r |
. . . . 5
β’ π
= (mStRedβπ) |
3 | 1, 2 | msrf 34200 |
. . . 4
β’ π
:(mPreStβπ)βΆ(mPreStβπ) |
4 | | ffn 6672 |
. . . 4
β’ (π
:(mPreStβπ)βΆ(mPreStβπ) β π
Fn (mPreStβπ)) |
5 | | fvelrnb 6907 |
. . . 4
β’ (π
Fn (mPreStβπ) β (π β ran π
β βπ β (mPreStβπ)(π
βπ ) = π)) |
6 | 3, 4, 5 | mp2b 10 |
. . 3
β’ (π β ran π
β βπ β (mPreStβπ)(π
βπ ) = π) |
7 | 1 | mpst123 34198 |
. . . . . . . . . . 11
β’ (π β (mPreStβπ) β π = β¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β©) |
8 | 7 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π β (mPreStβπ) β (π
βπ ) = (π
ββ¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β©)) |
9 | | id 22 |
. . . . . . . . . . . 12
β’ (π β (mPreStβπ) β π β (mPreStβπ)) |
10 | 7, 9 | eqeltrrd 2835 |
. . . . . . . . . . 11
β’ (π β (mPreStβπ) β β¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β© β
(mPreStβπ)) |
11 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(mVarsβπ) =
(mVarsβπ) |
12 | | eqid 2733 |
. . . . . . . . . . . 12
β’ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) = βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) |
13 | 11, 1, 2, 12 | msrval 34196 |
. . . . . . . . . . 11
β’
(β¨(1st β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β© β
(mPreStβπ) β
(π
ββ¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β©) =
β¨((1st β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
14 | 10, 13 | syl 17 |
. . . . . . . . . 10
β’ (π β (mPreStβπ) β (π
ββ¨(1st
β(1st βπ )), (2nd β(1st
βπ )), (2nd
βπ )β©) =
β¨((1st β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
15 | 8, 14 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β (mPreStβπ) β (π
βπ ) = β¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
16 | 3 | ffvelcdmi 7038 |
. . . . . . . . 9
β’ (π β (mPreStβπ) β (π
βπ ) β (mPreStβπ)) |
17 | 15, 16 | eqeltrrd 2835 |
. . . . . . . 8
β’ (π β (mPreStβπ) β β¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β© β (mPreStβπ)) |
18 | 11, 1, 2, 12 | msrval 34196 |
. . . . . . . 8
β’
(β¨((1st β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β© β (mPreStβπ) β (π
ββ¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) = β¨(((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
19 | 17, 18 | syl 17 |
. . . . . . 7
β’ (π β (mPreStβπ) β (π
ββ¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) = β¨(((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
20 | | inass 4183 |
. . . . . . . . . 10
β’
(((1st β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) = ((1st
β(1st βπ )) β© ((βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))))) |
21 | | inidm 4182 |
. . . . . . . . . . 11
β’ ((βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) = (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))) |
22 | 21 | ineq2i 4173 |
. . . . . . . . . 10
β’
((1st β(1st βπ )) β© ((βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))))) = ((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) |
23 | 20, 22 | eqtri 2761 |
. . . . . . . . 9
β’
(((1st β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) = ((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) |
24 | 23 | a1i 11 |
. . . . . . . 8
β’ (π β (mPreStβπ) β (((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) = ((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )}))))) |
25 | 24 | oteq1d 4846 |
. . . . . . 7
β’ (π β (mPreStβπ) β β¨(((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))) β© (βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β© = β¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
26 | 19, 25 | eqtrd 2773 |
. . . . . 6
β’ (π β (mPreStβπ) β (π
ββ¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) = β¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©) |
27 | 15 | fveq2d 6850 |
. . . . . 6
β’ (π β (mPreStβπ) β (π
β(π
βπ )) = (π
ββ¨((1st
β(1st βπ )) β© (βͺ
((mVarsβπ) β
((2nd β(1st βπ )) βͺ {(2nd βπ )})) Γ βͺ ((mVarsβπ) β ((2nd
β(1st βπ )) βͺ {(2nd βπ )})))), (2nd
β(1st βπ )), (2nd βπ )β©)) |
28 | 26, 27, 15 | 3eqtr4d 2783 |
. . . . 5
β’ (π β (mPreStβπ) β (π
β(π
βπ )) = (π
βπ )) |
29 | | fveq2 6846 |
. . . . . 6
β’ ((π
βπ ) = π β (π
β(π
βπ )) = (π
βπ)) |
30 | | id 22 |
. . . . . 6
β’ ((π
βπ ) = π β (π
βπ ) = π) |
31 | 29, 30 | eqeq12d 2749 |
. . . . 5
β’ ((π
βπ ) = π β ((π
β(π
βπ )) = (π
βπ ) β (π
βπ) = π)) |
32 | 28, 31 | syl5ibcom 244 |
. . . 4
β’ (π β (mPreStβπ) β ((π
βπ ) = π β (π
βπ) = π)) |
33 | 32 | rexlimiv 3142 |
. . 3
β’
(βπ β
(mPreStβπ)(π
βπ ) = π β (π
βπ) = π) |
34 | 6, 33 | sylbi 216 |
. 2
β’ (π β ran π
β (π
βπ) = π) |
35 | | mstaval.s |
. . 3
β’ π = (mStatβπ) |
36 | 2, 35 | mstaval 34202 |
. 2
β’ π = ran π
|
37 | 34, 36 | eleq2s 2852 |
1
β’ (π β π β (π
βπ) = π) |