Step | Hyp | Ref
| Expression |
1 | | eleq1 2825 |
. . . 4
β’ (π¦ = 0β β
(π¦ β (spanββͺ {π₯
β HAtoms β£ π₯
β π΄}) β
0β β (spanββͺ {π₯ β HAtoms β£ π₯ β π΄}))) |
2 | | shatomistic.1 |
. . . . . . . . 9
β’ π΄ β
Sβ |
3 | 2 | sheli 30042 |
. . . . . . . 8
β’ (π¦ β π΄ β π¦ β β) |
4 | | spansnsh 30389 |
. . . . . . . 8
β’ (π¦ β β β
(spanβ{π¦}) β
Sβ ) |
5 | | spanid 30175 |
. . . . . . . 8
β’
((spanβ{π¦})
β Sβ β (spanβ(spanβ{π¦})) = (spanβ{π¦})) |
6 | 3, 4, 5 | 3syl 18 |
. . . . . . 7
β’ (π¦ β π΄ β (spanβ(spanβ{π¦})) = (spanβ{π¦})) |
7 | 6 | adantr 481 |
. . . . . 6
β’ ((π¦ β π΄ β§ π¦ β 0β) β
(spanβ(spanβ{π¦})) = (spanβ{π¦})) |
8 | | spansna 31178 |
. . . . . . . . 9
β’ ((π¦ β β β§ π¦ β 0β)
β (spanβ{π¦})
β HAtoms) |
9 | 3, 8 | sylan 580 |
. . . . . . . 8
β’ ((π¦ β π΄ β§ π¦ β 0β) β
(spanβ{π¦}) β
HAtoms) |
10 | | spansnss 30399 |
. . . . . . . . . 10
β’ ((π΄ β
Sβ β§ π¦ β π΄) β (spanβ{π¦}) β π΄) |
11 | 2, 10 | mpan 688 |
. . . . . . . . 9
β’ (π¦ β π΄ β (spanβ{π¦}) β π΄) |
12 | 11 | adantr 481 |
. . . . . . . 8
β’ ((π¦ β π΄ β§ π¦ β 0β) β
(spanβ{π¦}) β
π΄) |
13 | | sseq1 3967 |
. . . . . . . . 9
β’ (π₯ = (spanβ{π¦}) β (π₯ β π΄ β (spanβ{π¦}) β π΄)) |
14 | 13 | elrab 3643 |
. . . . . . . 8
β’
((spanβ{π¦})
β {π₯ β HAtoms
β£ π₯ β π΄} β ((spanβ{π¦}) β HAtoms β§
(spanβ{π¦}) β
π΄)) |
15 | 9, 12, 14 | sylanbrc 583 |
. . . . . . 7
β’ ((π¦ β π΄ β§ π¦ β 0β) β
(spanβ{π¦}) β
{π₯ β HAtoms β£
π₯ β π΄}) |
16 | | elssuni 4896 |
. . . . . . 7
β’
((spanβ{π¦})
β {π₯ β HAtoms
β£ π₯ β π΄} β (spanβ{π¦}) β βͺ {π₯
β HAtoms β£ π₯
β π΄}) |
17 | | atssch 31171 |
. . . . . . . . . . 11
β’ HAtoms
β Cβ |
18 | | chsssh 30053 |
. . . . . . . . . . 11
β’
Cβ β
Sβ |
19 | 17, 18 | sstri 3951 |
. . . . . . . . . 10
β’ HAtoms
β Sβ |
20 | | rabss2 4033 |
. . . . . . . . . 10
β’ (HAtoms
β Sβ β {π₯ β HAtoms β£ π₯ β π΄} β {π₯ β Sβ
β£ π₯ β π΄}) |
21 | | uniss 4871 |
. . . . . . . . . 10
β’ ({π₯ β HAtoms β£ π₯ β π΄} β {π₯ β Sβ
β£ π₯ β π΄} β βͺ {π₯
β HAtoms β£ π₯
β π΄} β βͺ {π₯
β Sβ β£ π₯ β π΄}) |
22 | 19, 20, 21 | mp2b 10 |
. . . . . . . . 9
β’ βͺ {π₯
β HAtoms β£ π₯
β π΄} β βͺ {π₯
β Sβ β£ π₯ β π΄} |
23 | | unimax 4903 |
. . . . . . . . . . 11
β’ (π΄ β
Sβ β βͺ {π₯ β
Sβ β£ π₯ β π΄} = π΄) |
24 | 2, 23 | ax-mp 5 |
. . . . . . . . . 10
β’ βͺ {π₯
β Sβ β£ π₯ β π΄} = π΄ |
25 | 2 | shssii 30041 |
. . . . . . . . . 10
β’ π΄ β
β |
26 | 24, 25 | eqsstri 3976 |
. . . . . . . . 9
β’ βͺ {π₯
β Sβ β£ π₯ β π΄} β β |
27 | 22, 26 | sstri 3951 |
. . . . . . . 8
β’ βͺ {π₯
β HAtoms β£ π₯
β π΄} β
β |
28 | | spanss 30176 |
. . . . . . . 8
β’ ((βͺ {π₯
β HAtoms β£ π₯
β π΄} β β
β§ (spanβ{π¦})
β βͺ {π₯ β HAtoms β£ π₯ β π΄}) β (spanβ(spanβ{π¦})) β (spanββͺ {π₯
β HAtoms β£ π₯
β π΄})) |
29 | 27, 28 | mpan 688 |
. . . . . . 7
β’
((spanβ{π¦})
β βͺ {π₯ β HAtoms β£ π₯ β π΄} β (spanβ(spanβ{π¦})) β (spanββͺ {π₯
β HAtoms β£ π₯
β π΄})) |
30 | 15, 16, 29 | 3syl 18 |
. . . . . 6
β’ ((π¦ β π΄ β§ π¦ β 0β) β
(spanβ(spanβ{π¦})) β (spanββͺ {π₯
β HAtoms β£ π₯
β π΄})) |
31 | 7, 30 | eqsstrrd 3981 |
. . . . 5
β’ ((π¦ β π΄ β§ π¦ β 0β) β
(spanβ{π¦}) β
(spanββͺ {π₯ β HAtoms β£ π₯ β π΄})) |
32 | | spansnid 30391 |
. . . . . . 7
β’ (π¦ β β β π¦ β (spanβ{π¦})) |
33 | 3, 32 | syl 17 |
. . . . . 6
β’ (π¦ β π΄ β π¦ β (spanβ{π¦})) |
34 | 33 | adantr 481 |
. . . . 5
β’ ((π¦ β π΄ β§ π¦ β 0β) β π¦ β (spanβ{π¦})) |
35 | 31, 34 | sseldd 3943 |
. . . 4
β’ ((π¦ β π΄ β§ π¦ β 0β) β π¦ β (spanββͺ {π₯
β HAtoms β£ π₯
β π΄})) |
36 | | spancl 30164 |
. . . . . 6
β’ (βͺ {π₯
β HAtoms β£ π₯
β π΄} β β
β (spanββͺ {π₯ β HAtoms β£ π₯ β π΄}) β Sβ
) |
37 | | sh0 30044 |
. . . . . 6
β’
((spanββͺ {π₯ β HAtoms β£ π₯ β π΄}) β Sβ
β 0β β (spanββͺ
{π₯ β HAtoms β£
π₯ β π΄})) |
38 | 27, 36, 37 | mp2b 10 |
. . . . 5
β’
0β β (spanββͺ
{π₯ β HAtoms β£
π₯ β π΄}) |
39 | 38 | a1i 11 |
. . . 4
β’ (π¦ β π΄ β 0β β
(spanββͺ {π₯ β HAtoms β£ π₯ β π΄})) |
40 | 1, 35, 39 | pm2.61ne 3028 |
. . 3
β’ (π¦ β π΄ β π¦ β (spanββͺ {π₯
β HAtoms β£ π₯
β π΄})) |
41 | 40 | ssriv 3946 |
. 2
β’ π΄ β (spanββͺ {π₯
β HAtoms β£ π₯
β π΄}) |
42 | | spanss 30176 |
. . . 4
β’ ((βͺ {π₯
β Sβ β£ π₯ β π΄} β β β§ βͺ {π₯
β HAtoms β£ π₯
β π΄} β βͺ {π₯
β Sβ β£ π₯ β π΄}) β (spanββͺ {π₯
β HAtoms β£ π₯
β π΄}) β
(spanββͺ {π₯ β Sβ
β£ π₯ β π΄})) |
43 | 26, 22, 42 | mp2an 690 |
. . 3
β’
(spanββͺ {π₯ β HAtoms β£ π₯ β π΄}) β (spanββͺ {π₯
β Sβ β£ π₯ β π΄}) |
44 | 24 | fveq2i 6842 |
. . . 4
β’
(spanββͺ {π₯ β Sβ
β£ π₯ β π΄}) = (spanβπ΄) |
45 | | spanid 30175 |
. . . . 5
β’ (π΄ β
Sβ β (spanβπ΄) = π΄) |
46 | 2, 45 | ax-mp 5 |
. . . 4
β’
(spanβπ΄) =
π΄ |
47 | 44, 46 | eqtri 2764 |
. . 3
β’
(spanββͺ {π₯ β Sβ
β£ π₯ β π΄}) = π΄ |
48 | 43, 47 | sseqtri 3978 |
. 2
β’
(spanββͺ {π₯ β HAtoms β£ π₯ β π΄}) β π΄ |
49 | 41, 48 | eqssi 3958 |
1
β’ π΄ = (spanββͺ {π₯
β HAtoms β£ π₯
β π΄}) |