| Step | Hyp | Ref
| Expression |
|---|
| 1 | | df-salgen 45015 |
. . 3
β’ SalGen =
(π₯ β V β¦ β© {π
β SAlg β£ (βͺ π = βͺ π₯ β§ π₯ β π )}) |
| 2 | 1 | a1i 11 |
. 2
β’ (π β π β SalGen = (π₯ β V β¦ β© {π
β SAlg β£ (βͺ π = βͺ π₯ β§ π₯ β π )})) |
| 3 | | unieq 4918 |
. . . . . . 7
β’ (π₯ = π β βͺ π₯ = βͺ
π) |
| 4 | 3 | eqeq2d 2743 |
. . . . . 6
β’ (π₯ = π β (βͺ π = βͺ
π₯ β βͺ π =
βͺ π)) |
| 5 | | sseq1 4006 |
. . . . . 6
β’ (π₯ = π β (π₯ β π β π β π )) |
| 6 | 4, 5 | anbi12d 631 |
. . . . 5
β’ (π₯ = π β ((βͺ π = βͺ
π₯ β§ π₯ β π ) β (βͺ π = βͺ
π β§ π β π ))) |
| 7 | 6 | rabbidv 3440 |
. . . 4
β’ (π₯ = π β {π β SAlg β£ (βͺ π =
βͺ π₯ β§ π₯ β π )} = {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
| 8 | 7 | inteqd 4954 |
. . 3
β’ (π₯ = π β β© {π β SAlg β£ (βͺ π =
βͺ π₯ β§ π₯ β π )} = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
| 9 | 8 | adantl 482 |
. 2
β’ ((π β π β§ π₯ = π) β β© {π β SAlg β£ (βͺ π =
βͺ π₯ β§ π₯ β π )} = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
| 10 | | elex 3492 |
. 2
β’ (π β π β π β V) |
| 11 | | uniexg 7726 |
. . . . . . 7
β’ (π β π β βͺ π β V) |
| 12 | | pwsal 45017 |
. . . . . . 7
β’ (βͺ π
β V β π« βͺ π β SAlg) |
| 13 | 11, 12 | syl 17 |
. . . . . 6
β’ (π β π β π« βͺ π
β SAlg) |
| 14 | | unipw 5449 |
. . . . . . 7
β’ βͺ π« βͺ π = βͺ π |
| 15 | 14 | a1i 11 |
. . . . . 6
β’ (π β π β βͺ
π« βͺ π = βͺ π) |
| 16 | | pwuni 4948 |
. . . . . . 7
β’ π β π« βͺ π |
| 17 | 16 | a1i 11 |
. . . . . 6
β’ (π β π β π β π« βͺ π) |
| 18 | 13, 15, 17 | jca32 516 |
. . . . 5
β’ (π β π β (π« βͺ π
β SAlg β§ (βͺ π« βͺ π =
βͺ π β§ π β π« βͺ π))) |
| 19 | | unieq 4918 |
. . . . . . . 8
β’ (π = π« βͺ π
β βͺ π = βͺ π«
βͺ π) |
| 20 | 19 | eqeq1d 2734 |
. . . . . . 7
β’ (π = π« βͺ π
β (βͺ π = βͺ π β βͺ π« βͺ π = βͺ π)) |
| 21 | | sseq2 4007 |
. . . . . . 7
β’ (π = π« βͺ π
β (π β π β π β π« βͺ π)) |
| 22 | 20, 21 | anbi12d 631 |
. . . . . 6
β’ (π = π« βͺ π
β ((βͺ π = βͺ π β§ π β π ) β (βͺ
π« βͺ π = βͺ π β§ π β π« βͺ π))) |
| 23 | 22 | elrab 3682 |
. . . . 5
β’
(π« βͺ π β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β (π« βͺ π
β SAlg β§ (βͺ π« βͺ π =
βͺ π β§ π β π« βͺ π))) |
| 24 | 18, 23 | sylibr 233 |
. . . 4
β’ (π β π β π« βͺ π
β {π β SAlg
β£ (βͺ π = βͺ π β§ π β π )}) |
| 25 | 24 | ne0d 4334 |
. . 3
β’ (π β π β {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β β
) |
| 26 | | intex 5336 |
. . 3
β’ ({π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β β
β β© {π
β SAlg β£ (βͺ π = βͺ π β§ π β π )} β V) |
| 27 | 25, 26 | sylib 217 |
. 2
β’ (π β π β β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )} β V) |
| 28 | 2, 9, 10, 27 | fvmptd 7002 |
1
β’ (π β π β (SalGenβπ) = β© {π β SAlg β£ (βͺ π =
βͺ π β§ π β π )}) |
