Step | Hyp | Ref
| Expression |
1 | | df-salgen 44628 |
. . 3
β’ SalGen =
(π₯ β V β¦ β© {π
β SAlg β£ (βͺ π = βͺ π₯ β§ π₯ β π )}) |
2 | 1 | a1i 11 |
. 2
β’ (π β π β SalGen = (π₯ β V β¦ β© {π
β SAlg β£ (βͺ π = βͺ π₯ β§ π₯ β π )})) |
3 | | unieq 4881 |
. . . . . . 7
β’ (π₯ = π β βͺ π₯ = βͺ
π) |
4 | 3 | eqeq2d 2748 |
. . . . . 6
β’ (π₯ = π β (βͺ π = βͺ
π₯ β βͺ π =
βͺ π)) |
5 | | sseq1 3974 |
. . . . . 6
β’ (π₯ = π β (π₯ β π β π β π )) |
6 | 4, 5 | anbi12d 632 |
. . . . 5
β’ (π₯ = π β ((βͺ π = βͺ
π₯ β§ π₯ β π ) β (βͺ π = βͺ
π β§ π β π ))) |
7 | 6 | rabbidv 3418 |
. . . 4
β’ (π₯ = π β {π β SAlg β£ (βͺ π =
βͺ π₯ β§ π₯ β π )} = {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
8 | 7 | inteqd 4917 |
. . 3
β’ (π₯ = π β β© {π β SAlg β£ (βͺ π =
βͺ π₯ β§ π₯ β π )} = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
9 | 8 | adantl 483 |
. 2
β’ ((π β π β§ π₯ = π) β β© {π β SAlg β£ (βͺ π =
βͺ π₯ β§ π₯ β π )} = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
10 | | elex 3466 |
. 2
β’ (π β π β π β V) |
11 | | uniexg 7682 |
. . . . . . 7
β’ (π β π β βͺ π β V) |
12 | | pwsal 44630 |
. . . . . . 7
β’ (βͺ π
β V β π« βͺ π β SAlg) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ (π β π β π« βͺ π
β SAlg) |
14 | | unipw 5412 |
. . . . . . 7
β’ βͺ π« βͺ π = βͺ π |
15 | 14 | a1i 11 |
. . . . . 6
β’ (π β π β βͺ
π« βͺ π = βͺ π) |
16 | | pwuni 4911 |
. . . . . . 7
β’ π β π« βͺ π |
17 | 16 | a1i 11 |
. . . . . 6
β’ (π β π β π β π« βͺ π) |
18 | 13, 15, 17 | jca32 517 |
. . . . 5
β’ (π β π β (π« βͺ π
β SAlg β§ (βͺ π« βͺ π =
βͺ π β§ π β π« βͺ π))) |
19 | | unieq 4881 |
. . . . . . . 8
β’ (π = π« βͺ π
β βͺ π = βͺ π«
βͺ π) |
20 | 19 | eqeq1d 2739 |
. . . . . . 7
β’ (π = π« βͺ π
β (βͺ π = βͺ π β βͺ π« βͺ π = βͺ π)) |
21 | | sseq2 3975 |
. . . . . . 7
β’ (π = π« βͺ π
β (π β π β π β π« βͺ π)) |
22 | 20, 21 | anbi12d 632 |
. . . . . 6
β’ (π = π« βͺ π
β ((βͺ π = βͺ π β§ π β π ) β (βͺ
π« βͺ π = βͺ π β§ π β π« βͺ π))) |
23 | 22 | elrab 3650 |
. . . . 5
β’
(π« βͺ π β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β (π« βͺ π
β SAlg β§ (βͺ π« βͺ π =
βͺ π β§ π β π« βͺ π))) |
24 | 18, 23 | sylibr 233 |
. . . 4
β’ (π β π β π« βͺ π
β {π β SAlg
β£ (βͺ π = βͺ π β§ π β π )}) |
25 | 24 | ne0d 4300 |
. . 3
β’ (π β π β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β β
) |
26 | | intex 5299 |
. . 3
β’ ({π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β β
β β© {π
β SAlg β£ (βͺ π = βͺ π β§ π β π )} β V) |
27 | 25, 26 | sylib 217 |
. 2
β’ (π β π β β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β V) |
28 | 2, 9, 10, 27 | fvmptd 6960 |
1
β’ (π β π β (SalGenβπ) = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |