Step | Hyp | Ref
| Expression |
1 | | mstapst.p |
. . . . 5
β’ π = (mPreStβπ) |
2 | | mstapst.s |
. . . . 5
β’ π = (mStatβπ) |
3 | 1, 2 | mstapst 34527 |
. . . 4
β’ π β π |
4 | 3 | sseli 3978 |
. . 3
β’
(β¨π·, π», π΄β© β π β β¨π·, π», π΄β© β π) |
5 | | elmsta.v |
. . . . . . . . . 10
β’ π = (mVarsβπ) |
6 | | eqid 2733 |
. . . . . . . . . 10
β’
(mStRedβπ) =
(mStRedβπ) |
7 | | elmsta.z |
. . . . . . . . . 10
β’ π = βͺ
(π β (π» βͺ {π΄})) |
8 | 5, 1, 6, 7 | msrval 34518 |
. . . . . . . . 9
β’
(β¨π·, π», π΄β© β π β ((mStRedβπ)ββ¨π·, π», π΄β©) = β¨(π· β© (π Γ π)), π», π΄β©) |
9 | 4, 8 | syl 17 |
. . . . . . . 8
β’
(β¨π·, π», π΄β© β π β ((mStRedβπ)ββ¨π·, π», π΄β©) = β¨(π· β© (π Γ π)), π», π΄β©) |
10 | 6, 2 | msrid 34525 |
. . . . . . . 8
β’
(β¨π·, π», π΄β© β π β ((mStRedβπ)ββ¨π·, π», π΄β©) = β¨π·, π», π΄β©) |
11 | 9, 10 | eqtr3d 2775 |
. . . . . . 7
β’
(β¨π·, π», π΄β© β π β β¨(π· β© (π Γ π)), π», π΄β© = β¨π·, π», π΄β©) |
12 | 11 | fveq2d 6893 |
. . . . . 6
β’
(β¨π·, π», π΄β© β π β (1st ββ¨(π· β© (π Γ π)), π», π΄β©) = (1st ββ¨π·, π», π΄β©)) |
13 | 12 | fveq2d 6893 |
. . . . 5
β’
(β¨π·, π», π΄β© β π β (1st
β(1st ββ¨(π· β© (π Γ π)), π», π΄β©)) = (1st
β(1st ββ¨π·, π», π΄β©))) |
14 | | inss1 4228 |
. . . . . . 7
β’ (π· β© (π Γ π)) β π· |
15 | 1 | mpstrcl 34521 |
. . . . . . . . 9
β’
(β¨π·, π», π΄β© β π β (π· β V β§ π» β V β§ π΄ β V)) |
16 | 4, 15 | syl 17 |
. . . . . . . 8
β’
(β¨π·, π», π΄β© β π β (π· β V β§ π» β V β§ π΄ β V)) |
17 | 16 | simp1d 1143 |
. . . . . . 7
β’
(β¨π·, π», π΄β© β π β π· β V) |
18 | | ssexg 5323 |
. . . . . . 7
β’ (((π· β© (π Γ π)) β π· β§ π· β V) β (π· β© (π Γ π)) β V) |
19 | 14, 17, 18 | sylancr 588 |
. . . . . 6
β’
(β¨π·, π», π΄β© β π β (π· β© (π Γ π)) β V) |
20 | 16 | simp2d 1144 |
. . . . . 6
β’
(β¨π·, π», π΄β© β π β π» β V) |
21 | 16 | simp3d 1145 |
. . . . . 6
β’
(β¨π·, π», π΄β© β π β π΄ β V) |
22 | | ot1stg 7986 |
. . . . . 6
β’ (((π· β© (π Γ π)) β V β§ π» β V β§ π΄ β V) β (1st
β(1st ββ¨(π· β© (π Γ π)), π», π΄β©)) = (π· β© (π Γ π))) |
23 | 19, 20, 21, 22 | syl3anc 1372 |
. . . . 5
β’
(β¨π·, π», π΄β© β π β (1st
β(1st ββ¨(π· β© (π Γ π)), π», π΄β©)) = (π· β© (π Γ π))) |
24 | | ot1stg 7986 |
. . . . . 6
β’ ((π· β V β§ π» β V β§ π΄ β V) β
(1st β(1st ββ¨π·, π», π΄β©)) = π·) |
25 | 16, 24 | syl 17 |
. . . . 5
β’
(β¨π·, π», π΄β© β π β (1st
β(1st ββ¨π·, π», π΄β©)) = π·) |
26 | 13, 23, 25 | 3eqtr3d 2781 |
. . . 4
β’
(β¨π·, π», π΄β© β π β (π· β© (π Γ π)) = π·) |
27 | | inss2 4229 |
. . . 4
β’ (π· β© (π Γ π)) β (π Γ π) |
28 | 26, 27 | eqsstrrdi 4037 |
. . 3
β’
(β¨π·, π», π΄β© β π β π· β (π Γ π)) |
29 | 4, 28 | jca 513 |
. 2
β’
(β¨π·, π», π΄β© β π β (β¨π·, π», π΄β© β π β§ π· β (π Γ π))) |
30 | 8 | adantr 482 |
. . . . 5
β’
((β¨π·, π», π΄β© β π β§ π· β (π Γ π)) β ((mStRedβπ)ββ¨π·, π», π΄β©) = β¨(π· β© (π Γ π)), π», π΄β©) |
31 | | simpr 486 |
. . . . . . 7
β’
((β¨π·, π», π΄β© β π β§ π· β (π Γ π)) β π· β (π Γ π)) |
32 | | df-ss 3965 |
. . . . . . 7
β’ (π· β (π Γ π) β (π· β© (π Γ π)) = π·) |
33 | 31, 32 | sylib 217 |
. . . . . 6
β’
((β¨π·, π», π΄β© β π β§ π· β (π Γ π)) β (π· β© (π Γ π)) = π·) |
34 | 33 | oteq1d 4885 |
. . . . 5
β’
((β¨π·, π», π΄β© β π β§ π· β (π Γ π)) β β¨(π· β© (π Γ π)), π», π΄β© = β¨π·, π», π΄β©) |
35 | 30, 34 | eqtrd 2773 |
. . . 4
β’
((β¨π·, π», π΄β© β π β§ π· β (π Γ π)) β ((mStRedβπ)ββ¨π·, π», π΄β©) = β¨π·, π», π΄β©) |
36 | 1, 6 | msrf 34522 |
. . . . . 6
β’
(mStRedβπ):πβΆπ |
37 | | ffn 6715 |
. . . . . 6
β’
((mStRedβπ):πβΆπ β (mStRedβπ) Fn π) |
38 | 36, 37 | ax-mp 5 |
. . . . 5
β’
(mStRedβπ) Fn
π |
39 | | simpl 484 |
. . . . 5
β’
((β¨π·, π», π΄β© β π β§ π· β (π Γ π)) β β¨π·, π», π΄β© β π) |
40 | | fnfvelrn 7080 |
. . . . 5
β’
(((mStRedβπ)
Fn π β§ β¨π·, π», π΄β© β π) β ((mStRedβπ)ββ¨π·, π», π΄β©) β ran (mStRedβπ)) |
41 | 38, 39, 40 | sylancr 588 |
. . . 4
β’
((β¨π·, π», π΄β© β π β§ π· β (π Γ π)) β ((mStRedβπ)ββ¨π·, π», π΄β©) β ran (mStRedβπ)) |
42 | 35, 41 | eqeltrrd 2835 |
. . 3
β’
((β¨π·, π», π΄β© β π β§ π· β (π Γ π)) β β¨π·, π», π΄β© β ran (mStRedβπ)) |
43 | 6, 2 | mstaval 34524 |
. . 3
β’ π = ran (mStRedβπ) |
44 | 42, 43 | eleqtrrdi 2845 |
. 2
β’
((β¨π·, π», π΄β© β π β§ π· β (π Γ π)) β β¨π·, π», π΄β© β π) |
45 | 29, 44 | impbii 208 |
1
β’
(β¨π·, π», π΄β© β π β (β¨π·, π», π΄β© β π β§ π· β (π Γ π))) |