Step | Hyp | Ref
| Expression |
1 | | salgenuni.s |
. . . . 5
β’ π = (SalGenβπ) |
2 | 1 | a1i 11 |
. . . 4
β’ (π β π = (SalGenβπ)) |
3 | | salgenuni.x |
. . . . 5
β’ (π β π β π) |
4 | | salgenval 44715 |
. . . . 5
β’ (π β π β (SalGenβπ) = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π β (SalGenβπ) = β©
{π β SAlg β£
(βͺ π = βͺ π β§ π β π )}) |
6 | 2, 5 | eqtrd 2771 |
. . 3
β’ (π β π = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
7 | 6 | unieqd 4899 |
. 2
β’ (π β βͺ π =
βͺ β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
8 | | ssrab2 4057 |
. . . 4
β’ {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β SAlg |
9 | 8 | a1i 11 |
. . 3
β’ (π β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β SAlg) |
10 | | salgenn0 44725 |
. . . 4
β’ (π β π β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β β
) |
11 | 3, 10 | syl 17 |
. . 3
β’ (π β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β β
) |
12 | | unieq 4896 |
. . . . . . . . . 10
β’ (π = π‘ β βͺ π = βͺ
π‘) |
13 | 12 | eqeq1d 2733 |
. . . . . . . . 9
β’ (π = π‘ β (βͺ π = βͺ
π β βͺ π‘ =
βͺ π)) |
14 | | sseq2 3988 |
. . . . . . . . 9
β’ (π = π‘ β (π β π β π β π‘)) |
15 | 13, 14 | anbi12d 631 |
. . . . . . . 8
β’ (π = π‘ β ((βͺ π = βͺ
π β§ π β π ) β (βͺ π‘ = βͺ
π β§ π β π‘))) |
16 | 15 | elrab 3663 |
. . . . . . 7
β’ (π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β (π‘ β SAlg β§ (βͺ π‘ =
βͺ π β§ π β π‘))) |
17 | 16 | biimpi 215 |
. . . . . 6
β’ (π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β (π‘ β SAlg β§ (βͺ π‘ =
βͺ π β§ π β π‘))) |
18 | 17 | simprld 770 |
. . . . 5
β’ (π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β βͺ π‘ = βͺ
π) |
19 | | salgenuni.u |
. . . . . . 7
β’ π = βͺ
π |
20 | 19 | eqcomi 2740 |
. . . . . 6
β’ βͺ π =
π |
21 | 20 | a1i 11 |
. . . . 5
β’ (π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β βͺ π = π) |
22 | 18, 21 | eqtrd 2771 |
. . . 4
β’ (π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β βͺ π‘ = π) |
23 | 22 | adantl 482 |
. . 3
β’ ((π β§ π‘ β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) β βͺ π‘ = π) |
24 | 9, 11, 23 | intsaluni 44723 |
. 2
β’ (π β βͺ β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} = π) |
25 | 7, 24 | eqtrd 2771 |
1
β’ (π β βͺ π =
π) |