Step | Hyp | Ref
| Expression |
1 | | opelxp 5673 |
. . 3
β’
(β¨β¨π·,
π»β©, π΄β© β (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ) β (β¨π·, π»β© β ({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) β§ π΄ β πΈ)) |
2 | | opelxp 5673 |
. . . . 5
β’
(β¨π·, π»β© β ({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) β (π· β {π β π« π β£ β‘π = π} β§ π» β (π« πΈ β© Fin))) |
3 | | cnveq 5833 |
. . . . . . . . 9
β’ (π = π· β β‘π = β‘π·) |
4 | | id 22 |
. . . . . . . . 9
β’ (π = π· β π = π·) |
5 | 3, 4 | eqeq12d 2749 |
. . . . . . . 8
β’ (π = π· β (β‘π = π β β‘π· = π·)) |
6 | 5 | elrab 3649 |
. . . . . . 7
β’ (π· β {π β π« π β£ β‘π = π} β (π· β π« π β§ β‘π· = π·)) |
7 | | mpstval.v |
. . . . . . . . . 10
β’ π = (mDVβπ) |
8 | 7 | fvexi 6860 |
. . . . . . . . 9
β’ π β V |
9 | 8 | elpw2 5306 |
. . . . . . . 8
β’ (π· β π« π β π· β π) |
10 | 9 | anbi1i 625 |
. . . . . . 7
β’ ((π· β π« π β§ β‘π· = π·) β (π· β π β§ β‘π· = π·)) |
11 | 6, 10 | bitri 275 |
. . . . . 6
β’ (π· β {π β π« π β£ β‘π = π} β (π· β π β§ β‘π· = π·)) |
12 | | elfpw 9304 |
. . . . . 6
β’ (π» β (π« πΈ β© Fin) β (π» β πΈ β§ π» β Fin)) |
13 | 11, 12 | anbi12i 628 |
. . . . 5
β’ ((π· β {π β π« π β£ β‘π = π} β§ π» β (π« πΈ β© Fin)) β ((π· β π β§ β‘π· = π·) β§ (π» β πΈ β§ π» β Fin))) |
14 | 2, 13 | bitri 275 |
. . . 4
β’
(β¨π·, π»β© β ({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) β ((π· β π β§ β‘π· = π·) β§ (π» β πΈ β§ π» β Fin))) |
15 | 14 | anbi1i 625 |
. . 3
β’
((β¨π·, π»β© β ({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) β§ π΄ β πΈ) β (((π· β π β§ β‘π· = π·) β§ (π» β πΈ β§ π» β Fin)) β§ π΄ β πΈ)) |
16 | 1, 15 | bitri 275 |
. 2
β’
(β¨β¨π·,
π»β©, π΄β© β (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ) β (((π· β π β§ β‘π· = π·) β§ (π» β πΈ β§ π» β Fin)) β§ π΄ β πΈ)) |
17 | | df-ot 4599 |
. . 3
β’
β¨π·, π», π΄β© = β¨β¨π·, π»β©, π΄β© |
18 | | mpstval.e |
. . . 4
β’ πΈ = (mExβπ) |
19 | | mpstval.p |
. . . 4
β’ π = (mPreStβπ) |
20 | 7, 18, 19 | mpstval 34193 |
. . 3
β’ π = (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ) |
21 | 17, 20 | eleq12i 2827 |
. 2
β’
(β¨π·, π», π΄β© β π β β¨β¨π·, π»β©, π΄β© β (({π β π« π β£ β‘π = π} Γ (π« πΈ β© Fin)) Γ πΈ)) |
22 | | df-3an 1090 |
. 2
β’ (((π· β π β§ β‘π· = π·) β§ (π» β πΈ β§ π» β Fin) β§ π΄ β πΈ) β (((π· β π β§ β‘π· = π·) β§ (π» β πΈ β§ π» β Fin)) β§ π΄ β πΈ)) |
23 | 16, 21, 22 | 3bitr4i 303 |
1
β’
(β¨π·, π», π΄β© β π β ((π· β π β§ β‘π· = π·) β§ (π» β πΈ β§ π» β Fin) β§ π΄ β πΈ)) |