Step | Hyp | Ref
| Expression |
1 | | lsatset.a |
. 2
⊢ 𝐴 = (LSAtoms‘𝑊) |
2 | | elex 3185 |
. . 3
⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) |
3 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
4 | | lsatset.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) |
5 | 3, 4 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
6 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = (0g‘𝑊)) |
7 | | lsatset.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑊) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (0g‘𝑤) = 0 ) |
9 | 8 | sneqd 4137 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → {(0g‘𝑤)} = { 0 }) |
10 | 5, 9 | difeq12d 3691 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((Base‘𝑤) ∖ {(0g‘𝑤)}) = (𝑉 ∖ { 0 })) |
11 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊)) |
12 | | lsatset.n |
. . . . . . . 8
⊢ 𝑁 = (LSpan‘𝑊) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝑁) |
14 | 13 | fveq1d 6105 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((LSpan‘𝑤)‘{𝑣}) = (𝑁‘{𝑣})) |
15 | 10, 14 | mpteq12dv 4663 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})) = (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |
16 | 15 | rneqd 5274 |
. . . 4
⊢ (𝑤 = 𝑊 → ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})) = ran (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |
17 | | df-lsatoms 33281 |
. . . 4
⊢ LSAtoms =
(𝑤 ∈ V ↦ ran
(𝑣 ∈
((Base‘𝑤) ∖
{(0g‘𝑤)})
↦ ((LSpan‘𝑤)‘{𝑣}))) |
18 | | fvex 6113 |
. . . . . . . 8
⊢
(LSpan‘𝑊)
∈ V |
19 | 12, 18 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑁 ∈ V |
20 | 19 | rnex 6992 |
. . . . . 6
⊢ ran 𝑁 ∈ V |
21 | | p0ex 4779 |
. . . . . 6
⊢ {∅}
∈ V |
22 | 20, 21 | unex 6854 |
. . . . 5
⊢ (ran
𝑁 ∪ {∅}) ∈
V |
23 | | eqid 2610 |
. . . . . . 7
⊢ (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) = (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) |
24 | | fvrn0 6126 |
. . . . . . . 8
⊢ (𝑁‘{𝑣}) ∈ (ran 𝑁 ∪ {∅}) |
25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝑣 ∈ (𝑉 ∖ { 0 }) → (𝑁‘{𝑣}) ∈ (ran 𝑁 ∪ {∅})) |
26 | 23, 25 | fmpti 6291 |
. . . . . 6
⊢ (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})):(𝑉 ∖ { 0 })⟶(ran 𝑁 ∪
{∅}) |
27 | | frn 5966 |
. . . . . 6
⊢ ((𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})):(𝑉 ∖ { 0 })⟶(ran 𝑁 ∪ {∅}) → ran
(𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) ⊆ (ran 𝑁 ∪ {∅})) |
28 | 26, 27 | ax-mp 5 |
. . . . 5
⊢ ran
(𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) ⊆ (ran 𝑁 ∪ {∅}) |
29 | 22, 28 | ssexi 4731 |
. . . 4
⊢ ran
(𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣})) ∈ V |
30 | 16, 17, 29 | fvmpt 6191 |
. . 3
⊢ (𝑊 ∈ V →
(LSAtoms‘𝑊) = ran
(𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |
31 | 2, 30 | syl 17 |
. 2
⊢ (𝑊 ∈ 𝑋 → (LSAtoms‘𝑊) = ran (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |
32 | 1, 31 | syl5eq 2656 |
1
⊢ (𝑊 ∈ 𝑋 → 𝐴 = ran (𝑣 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑣}))) |