Step | Hyp | Ref
| Expression |
1 | | lsatset.a |
. 2
β’ π΄ = (LSAtomsβπ) |
2 | | elex 3466 |
. . 3
β’ (π β π β π β V) |
3 | | fveq2 6847 |
. . . . . . . 8
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
4 | | lsatset.v |
. . . . . . . 8
β’ π = (Baseβπ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β (Baseβπ€) = π) |
6 | | fveq2 6847 |
. . . . . . . . 9
β’ (π€ = π β (0gβπ€) = (0gβπ)) |
7 | | lsatset.z |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . . . 8
β’ (π€ = π β (0gβπ€) = 0 ) |
9 | 8 | sneqd 4603 |
. . . . . . 7
β’ (π€ = π β {(0gβπ€)} = { 0 }) |
10 | 5, 9 | difeq12d 4088 |
. . . . . 6
β’ (π€ = π β ((Baseβπ€) β {(0gβπ€)}) = (π β { 0 })) |
11 | | fveq2 6847 |
. . . . . . . 8
β’ (π€ = π β (LSpanβπ€) = (LSpanβπ)) |
12 | | lsatset.n |
. . . . . . . 8
β’ π = (LSpanβπ) |
13 | 11, 12 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β (LSpanβπ€) = π) |
14 | 13 | fveq1d 6849 |
. . . . . 6
β’ (π€ = π β ((LSpanβπ€)β{π£}) = (πβ{π£})) |
15 | 10, 14 | mpteq12dv 5201 |
. . . . 5
β’ (π€ = π β (π£ β ((Baseβπ€) β {(0gβπ€)}) β¦ ((LSpanβπ€)β{π£})) = (π£ β (π β { 0 }) β¦ (πβ{π£}))) |
16 | 15 | rneqd 5898 |
. . . 4
β’ (π€ = π β ran (π£ β ((Baseβπ€) β {(0gβπ€)}) β¦ ((LSpanβπ€)β{π£})) = ran (π£ β (π β { 0 }) β¦ (πβ{π£}))) |
17 | | df-lsatoms 37467 |
. . . 4
β’ LSAtoms =
(π€ β V β¦ ran
(π£ β
((Baseβπ€) β
{(0gβπ€)})
β¦ ((LSpanβπ€)β{π£}))) |
18 | 12 | fvexi 6861 |
. . . . . . 7
β’ π β V |
19 | 18 | rnex 7854 |
. . . . . 6
β’ ran π β V |
20 | | p0ex 5344 |
. . . . . 6
β’ {β
}
β V |
21 | 19, 20 | unex 7685 |
. . . . 5
β’ (ran
π βͺ {β
}) β
V |
22 | | eqid 2737 |
. . . . . . 7
β’ (π£ β (π β { 0 }) β¦ (πβ{π£})) = (π£ β (π β { 0 }) β¦ (πβ{π£})) |
23 | | fvrn0 6877 |
. . . . . . . 8
β’ (πβ{π£}) β (ran π βͺ {β
}) |
24 | 23 | a1i 11 |
. . . . . . 7
β’ (π£ β (π β { 0 }) β (πβ{π£}) β (ran π βͺ {β
})) |
25 | 22, 24 | fmpti 7065 |
. . . . . 6
β’ (π£ β (π β { 0 }) β¦ (πβ{π£})):(π β { 0 })βΆ(ran π βͺ
{β
}) |
26 | | frn 6680 |
. . . . . 6
β’ ((π£ β (π β { 0 }) β¦ (πβ{π£})):(π β { 0 })βΆ(ran π βͺ {β
}) β ran
(π£ β (π β { 0 }) β¦ (πβ{π£})) β (ran π βͺ {β
})) |
27 | 25, 26 | ax-mp 5 |
. . . . 5
β’ ran
(π£ β (π β { 0 }) β¦ (πβ{π£})) β (ran π βͺ {β
}) |
28 | 21, 27 | ssexi 5284 |
. . . 4
β’ ran
(π£ β (π β { 0 }) β¦ (πβ{π£})) β V |
29 | 16, 17, 28 | fvmpt 6953 |
. . 3
β’ (π β V β
(LSAtomsβπ) = ran
(π£ β (π β { 0 }) β¦ (πβ{π£}))) |
30 | 2, 29 | syl 17 |
. 2
β’ (π β π β (LSAtomsβπ) = ran (π£ β (π β { 0 }) β¦ (πβ{π£}))) |
31 | 1, 30 | eqtrid 2789 |
1
β’ (π β π β π΄ = ran (π£ β (π β { 0 }) β¦ (πβ{π£}))) |