| Step | Hyp | Ref
| Expression |
| 1 | | lsatset.a |
. 2
⊢ 𝐴 = (LSAtoms‘𝑊) |
| 2 | | elex 3501 |
. . 3
⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) |
| 3 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
| 4 | | lsatset.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) |
| 5 | 3, 4 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
| 6 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊)) |
| 7 | | lsatset.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑊) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 ) |
| 9 | 8 | sneqd 4638 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → {(0g‘𝑤)} = { 0 }) |
| 10 | 5, 9 | difeq12d 4127 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((Base‘𝑤) ∖ {(0g‘𝑤)}) = (𝑉 ∖ { 0 })) |
| 11 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊)) |
| 12 | | lsatset.n |
. . . . . . . 8
⊢ 𝑁 = (LSpan‘𝑊) |
| 13 | 11, 12 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝑁) |
| 14 | 13 | fveq1d 6908 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((LSpan‘𝑤)‘{𝑣}) = (𝑁‘{𝑣})) |
| 15 | 10, 14 | mpteq12dv 5233 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})) = (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |
| 16 | 15 | rneqd 5949 |
. . . 4
⊢ (𝑤 = 𝑊 → ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})) = ran (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |
| 17 | | df-lsatoms 38977 |
. . . 4
⊢ LSAtoms =
(𝑤 ∈ V ↦ ran
(𝑣 ∈
((Base‘𝑤) ∖
{(0g‘𝑤)})
↦ ((LSpan‘𝑤)‘{𝑣}))) |
| 18 | 12 | fvexi 6920 |
. . . . . . 7
⊢ 𝑁 ∈ V |
| 19 | 18 | rnex 7932 |
. . . . . 6
⊢ ran 𝑁 ∈ V |
| 20 | | p0ex 5384 |
. . . . . 6
⊢ {∅}
∈ V |
| 21 | 19, 20 | unex 7764 |
. . . . 5
⊢ (ran
𝑁 ∪ {∅}) ∈
V |
| 22 | | eqid 2737 |
. . . . . . 7
⊢ (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) = (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) |
| 23 | | fvrn0 6936 |
. . . . . . . 8
⊢ (𝑁‘{𝑣}) ∈ (ran 𝑁 ∪ {∅}) |
| 24 | 23 | a1i 11 |
. . . . . . 7
⊢ (𝑣 ∈ (𝑉 ∖ { 0 }) → (𝑁‘{𝑣}) ∈ (ran 𝑁 ∪ {∅})) |
| 25 | 22, 24 | fmpti 7132 |
. . . . . 6
⊢ (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})):(𝑉 ∖ { 0 })⟶(ran 𝑁 ∪
{∅}) |
| 26 | | frn 6743 |
. . . . . 6
⊢ ((𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})):(𝑉 ∖ { 0 })⟶(ran 𝑁 ∪ {∅}) → ran
(𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) ⊆ (ran 𝑁 ∪ {∅})) |
| 27 | 25, 26 | ax-mp 5 |
. . . . 5
⊢ ran
(𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) ⊆ (ran 𝑁 ∪ {∅}) |
| 28 | 21, 27 | ssexi 5322 |
. . . 4
⊢ ran
(𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) ∈ V |
| 29 | 16, 17, 28 | fvmpt 7016 |
. . 3
⊢ (𝑊 ∈ V →
(LSAtoms‘𝑊) = ran
(𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |
| 30 | 2, 29 | syl 17 |
. 2
⊢ (𝑊 ∈ 𝑋 → (LSAtoms‘𝑊) = ran (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |
| 31 | 1, 30 | eqtrid 2789 |
1
⊢ (𝑊 ∈ 𝑋 → 𝐴 = ran (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |