| Step | Hyp | Ref
| Expression |
|---|
| 1 | | salgenval 44715 |
. 2
β’ (π β π β (SalGenβπ) = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
| 2 | | ssrab2 4057 |
. . . 4
β’ {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β SAlg |
| 3 | 2 | a1i 11 |
. . 3
β’ (π β π β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β SAlg) |
| 4 | | salgenn0 44725 |
. . 3
β’ (π β π β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β β
) |
| 5 | | unieq 4896 |
. . . . . . . . 9
β’ (π = π‘ β βͺ π = βͺ
π‘) |
| 6 | 5 | eqeq1d 2733 |
. . . . . . . 8
β’ (π = π‘ β (βͺ π = βͺ
π β βͺ π‘ =
βͺ π)) |
| 7 | | sseq2 3988 |
. . . . . . . 8
β’ (π = π‘ β (π β π β π β π‘)) |
| 8 | 6, 7 | anbi12d 631 |
. . . . . . 7
β’ (π = π‘ β ((βͺ π = βͺ
π β§ π β π ) β (βͺ π‘ = βͺ
π β§ π β π‘))) |
| 9 | 8 | elrab 3663 |
. . . . . 6
β’ (π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β (π‘ β SAlg β§ (βͺ π‘ =
βͺ π β§ π β π‘))) |
| 10 | 9 | biimpi 215 |
. . . . 5
β’ (π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β (π‘ β SAlg β§ (βͺ π‘ =
βͺ π β§ π β π‘))) |
| 11 | 10 | simprld 770 |
. . . 4
β’ (π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β βͺ π‘ = βͺ
π) |
| 12 | 11 | adantl 482 |
. . 3
β’ ((π β π β§ π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) β βͺ π‘ = βͺ
π) |
| 13 | 3, 4, 12 | intsal 44724 |
. 2
β’ (π β π β β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β SAlg) |
| 14 | 1, 13 | eqeltrd 2832 |
1
β’ (π β π β (SalGenβπ) β SAlg) |
