Step | Hyp | Ref
| Expression |
1 | | issalgend.x |
. . 3
β’ (π β π β π) |
2 | | eqid 2732 |
. . 3
β’
(SalGenβπ) =
(SalGenβπ) |
3 | | issalgend.s |
. . 3
β’ (π β π β SAlg) |
4 | | issalgend.i |
. . 3
β’ (π β π β π) |
5 | | issalgend.u |
. . 3
β’ (π β βͺ π =
βͺ π) |
6 | 1, 2, 3, 4, 5 | salgenss 44667 |
. 2
β’ (π β (SalGenβπ) β π) |
7 | | simpl 484 |
. . . . . 6
β’ ((π β§ π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) β π) |
8 | | elrabi 3643 |
. . . . . . 7
β’ (π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β π¦ β SAlg) |
9 | 8 | adantl 483 |
. . . . . 6
β’ ((π β§ π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) β π¦ β SAlg) |
10 | | unieq 4880 |
. . . . . . . . . . . 12
β’ (π = π¦ β βͺ π = βͺ
π¦) |
11 | 10 | eqeq1d 2734 |
. . . . . . . . . . 11
β’ (π = π¦ β (βͺ π = βͺ
π β βͺ π¦ =
βͺ π)) |
12 | | sseq2 3974 |
. . . . . . . . . . 11
β’ (π = π¦ β (π β π β π β π¦)) |
13 | 11, 12 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = π¦ β ((βͺ π = βͺ
π β§ π β π ) β (βͺ π¦ = βͺ
π β§ π β π¦))) |
14 | 13 | elrab 3649 |
. . . . . . . . 9
β’ (π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β (π¦ β SAlg β§ (βͺ π¦ =
βͺ π β§ π β π¦))) |
15 | 14 | biimpi 215 |
. . . . . . . 8
β’ (π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β (π¦ β SAlg β§ (βͺ π¦ =
βͺ π β§ π β π¦))) |
16 | 15 | simprld 771 |
. . . . . . 7
β’ (π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β βͺ π¦ = βͺ
π) |
17 | 16 | adantl 483 |
. . . . . 6
β’ ((π β§ π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) β βͺ π¦ = βͺ
π) |
18 | 15 | simprrd 773 |
. . . . . . 7
β’ (π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β π β π¦) |
19 | 18 | adantl 483 |
. . . . . 6
β’ ((π β§ π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) β π β π¦) |
20 | | issalgend.a |
. . . . . 6
β’ ((π β§ (π¦ β SAlg β§ βͺ π¦ =
βͺ π β§ π β π¦)) β π β π¦) |
21 | 7, 9, 17, 19, 20 | syl13anc 1373 |
. . . . 5
β’ ((π β§ π¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) β π β π¦) |
22 | 21 | ralrimiva 3140 |
. . . 4
β’ (π β βπ¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}π β π¦) |
23 | | ssint 4929 |
. . . 4
β’ (π β β© {π
β SAlg β£ (βͺ π = βͺ π β§ π β π )} β βπ¦ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}π β π¦) |
24 | 22, 23 | sylibr 233 |
. . 3
β’ (π β π β β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
25 | | salgenval 44652 |
. . . 4
β’ (π β π β (SalGenβπ) = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
26 | 1, 25 | syl 17 |
. . 3
β’ (π β (SalGenβπ) = β©
{π β SAlg β£
(βͺ π = βͺ π β§ π β π )}) |
27 | 24, 26 | sseqtrrd 3989 |
. 2
β’ (π β π β (SalGenβπ)) |
28 | 6, 27 | eqssd 3965 |
1
β’ (π β (SalGenβπ) = π) |