Step | Hyp | Ref
| Expression |
1 | | sseq1 3970 |
. . . . . 6
β’ (π₯ = β
β (π₯ β π΄ β β
β π΄)) |
2 | 1 | anbi2d 630 |
. . . . 5
β’ (π₯ = β
β ((πΎ β HL β§ π₯ β π΄) β (πΎ β HL β§ β
β π΄))) |
3 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = β
β (πβπ₯) = (πββ
)) |
4 | 3 | eleq1d 2823 |
. . . . 5
β’ (π₯ = β
β ((πβπ₯) β π β (πββ
) β π)) |
5 | 2, 4 | imbi12d 345 |
. . . 4
β’ (π₯ = β
β (((πΎ β HL β§ π₯ β π΄) β (πβπ₯) β π) β ((πΎ β HL β§ β
β π΄) β (πββ
) β π))) |
6 | | sseq1 3970 |
. . . . . 6
β’ (π₯ = π¦ β (π₯ β π΄ β π¦ β π΄)) |
7 | 6 | anbi2d 630 |
. . . . 5
β’ (π₯ = π¦ β ((πΎ β HL β§ π₯ β π΄) β (πΎ β HL β§ π¦ β π΄))) |
8 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = π¦ β (πβπ₯) = (πβπ¦)) |
9 | 8 | eleq1d 2823 |
. . . . 5
β’ (π₯ = π¦ β ((πβπ₯) β π β (πβπ¦) β π)) |
10 | 7, 9 | imbi12d 345 |
. . . 4
β’ (π₯ = π¦ β (((πΎ β HL β§ π₯ β π΄) β (πβπ₯) β π) β ((πΎ β HL β§ π¦ β π΄) β (πβπ¦) β π))) |
11 | | sseq1 3970 |
. . . . . 6
β’ (π₯ = (π¦ βͺ {π§}) β (π₯ β π΄ β (π¦ βͺ {π§}) β π΄)) |
12 | 11 | anbi2d 630 |
. . . . 5
β’ (π₯ = (π¦ βͺ {π§}) β ((πΎ β HL β§ π₯ β π΄) β (πΎ β HL β§ (π¦ βͺ {π§}) β π΄))) |
13 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = (π¦ βͺ {π§}) β (πβπ₯) = (πβ(π¦ βͺ {π§}))) |
14 | 13 | eleq1d 2823 |
. . . . 5
β’ (π₯ = (π¦ βͺ {π§}) β ((πβπ₯) β π β (πβ(π¦ βͺ {π§})) β π)) |
15 | 12, 14 | imbi12d 345 |
. . . 4
β’ (π₯ = (π¦ βͺ {π§}) β (((πΎ β HL β§ π₯ β π΄) β (πβπ₯) β π) β ((πΎ β HL β§ (π¦ βͺ {π§}) β π΄) β (πβ(π¦ βͺ {π§})) β π))) |
16 | | sseq1 3970 |
. . . . . 6
β’ (π₯ = π β (π₯ β π΄ β π β π΄)) |
17 | 16 | anbi2d 630 |
. . . . 5
β’ (π₯ = π β ((πΎ β HL β§ π₯ β π΄) β (πΎ β HL β§ π β π΄))) |
18 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
19 | 18 | eleq1d 2823 |
. . . . 5
β’ (π₯ = π β ((πβπ₯) β π β (πβπ) β π)) |
20 | 17, 19 | imbi12d 345 |
. . . 4
β’ (π₯ = π β (((πΎ β HL β§ π₯ β π΄) β (πβπ₯) β π) β ((πΎ β HL β§ π β π΄) β (πβπ) β π))) |
21 | | pclfincl.c |
. . . . . . 7
β’ π = (PClβπΎ) |
22 | 21 | pcl0N 38388 |
. . . . . 6
β’ (πΎ β HL β (πββ
) =
β
) |
23 | | pclfincl.s |
. . . . . . 7
β’ π = (PSubClβπΎ) |
24 | 23 | 0psubclN 38409 |
. . . . . 6
β’ (πΎ β HL β β
β
π) |
25 | 22, 24 | eqeltrd 2838 |
. . . . 5
β’ (πΎ β HL β (πββ
) β π) |
26 | 25 | adantr 482 |
. . . 4
β’ ((πΎ β HL β§ β
β
π΄) β (πββ
) β π) |
27 | | anass 470 |
. . . . . . 7
β’ (((πΎ β HL β§ π¦ β π΄) β§ π§ β π΄) β (πΎ β HL β§ (π¦ β π΄ β§ π§ β π΄))) |
28 | | vex 3450 |
. . . . . . . . . . 11
β’ π§ β V |
29 | 28 | snss 4747 |
. . . . . . . . . 10
β’ (π§ β π΄ β {π§} β π΄) |
30 | 29 | anbi2i 624 |
. . . . . . . . 9
β’ ((π¦ β π΄ β§ π§ β π΄) β (π¦ β π΄ β§ {π§} β π΄)) |
31 | | unss 4145 |
. . . . . . . . 9
β’ ((π¦ β π΄ β§ {π§} β π΄) β (π¦ βͺ {π§}) β π΄) |
32 | 30, 31 | bitri 275 |
. . . . . . . 8
β’ ((π¦ β π΄ β§ π§ β π΄) β (π¦ βͺ {π§}) β π΄) |
33 | 32 | anbi2i 624 |
. . . . . . 7
β’ ((πΎ β HL β§ (π¦ β π΄ β§ π§ β π΄)) β (πΎ β HL β§ (π¦ βͺ {π§}) β π΄)) |
34 | 27, 33 | bitr2i 276 |
. . . . . 6
β’ ((πΎ β HL β§ (π¦ βͺ {π§}) β π΄) β ((πΎ β HL β§ π¦ β π΄) β§ π§ β π΄)) |
35 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β π¦ = β
) |
36 | 35 | uneq1d 4123 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π¦ βͺ {π§}) = (β
βͺ {π§})) |
37 | | uncom 4114 |
. . . . . . . . . . . . . . 15
β’ (β
βͺ {π§}) = ({π§} βͺ
β
) |
38 | | un0 4351 |
. . . . . . . . . . . . . . 15
β’ ({π§} βͺ β
) = {π§} |
39 | 37, 38 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’ (β
βͺ {π§}) = {π§} |
40 | 36, 39 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π¦ βͺ {π§}) = {π§}) |
41 | 40 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβ(π¦ βͺ {π§})) = (πβ{π§})) |
42 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β πΎ β HL) |
43 | | hlatl 37825 |
. . . . . . . . . . . . . . 15
β’ (πΎ β HL β πΎ β AtLat) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β πΎ β AtLat) |
45 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β π§ β π΄) |
46 | | pclfincl.a |
. . . . . . . . . . . . . . 15
β’ π΄ = (AtomsβπΎ) |
47 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(PSubSpβπΎ) =
(PSubSpβπΎ) |
48 | 46, 47 | snatpsubN 38216 |
. . . . . . . . . . . . . 14
β’ ((πΎ β AtLat β§ π§ β π΄) β {π§} β (PSubSpβπΎ)) |
49 | 44, 45, 48 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β {π§} β (PSubSpβπΎ)) |
50 | 47, 21 | pclidN 38362 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ {π§} β (PSubSpβπΎ)) β (πβ{π§}) = {π§}) |
51 | 42, 49, 50 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβ{π§}) = {π§}) |
52 | 41, 51 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβ(π¦ βͺ {π§})) = {π§}) |
53 | 46, 23 | atpsubclN 38411 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π§ β π΄) β {π§} β π) |
54 | 42, 45, 53 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β {π§} β π) |
55 | 52, 54 | eqeltrd 2838 |
. . . . . . . . . 10
β’ ((((π¦ β Fin β§ π¦ = β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβ(π¦ βͺ {π§})) β π) |
56 | 55 | exp43 438 |
. . . . . . . . 9
β’ ((π¦ β Fin β§ π¦ = β
) β ((πΎ β HL β§ π¦ β π΄) β ((πβπ¦) β π β (π§ β π΄ β (πβ(π¦ βͺ {π§})) β π)))) |
57 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β πΎ β HL) |
58 | 46, 21 | pclssidN 38361 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β HL β§ π¦ β π΄) β π¦ β (πβπ¦)) |
59 | 58 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β π¦ β (πβπ¦)) |
60 | | unss1 4140 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (πβπ¦) β (π¦ βͺ {π§}) β ((πβπ¦) βͺ {π§})) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π¦ βͺ {π§}) β ((πβπ¦) βͺ {π§})) |
62 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβπ¦) β π) |
63 | 46, 23 | psubclssatN 38407 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β HL β§ (πβπ¦) β π) β (πβπ¦) β π΄) |
64 | 57, 62, 63 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβπ¦) β π΄) |
65 | | snssi 4769 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β π΄ β {π§} β π΄) |
66 | 65 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β {π§} β π΄) |
67 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(+πβπΎ) = (+πβπΎ) |
68 | 46, 67 | paddunssN 38274 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ (πβπ¦) β π΄ β§ {π§} β π΄) β ((πβπ¦) βͺ {π§}) β ((πβπ¦)(+πβπΎ){π§})) |
69 | 57, 64, 66, 68 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β ((πβπ¦) βͺ {π§}) β ((πβπ¦)(+πβπΎ){π§})) |
70 | 61, 69 | sstrd 3955 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π¦ βͺ {π§}) β ((πβπ¦)(+πβπΎ){π§})) |
71 | 46, 67 | paddssat 38280 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ (πβπ¦) β π΄ β§ {π§} β π΄) β ((πβπ¦)(+πβπΎ){π§}) β π΄) |
72 | 57, 64, 66, 71 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β ((πβπ¦)(+πβπΎ){π§}) β π΄) |
73 | 46, 21 | pclssN 38360 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π¦ βͺ {π§}) β ((πβπ¦)(+πβπΎ){π§}) β§ ((πβπ¦)(+πβπΎ){π§}) β π΄) β (πβ(π¦ βͺ {π§})) β (πβ((πβπ¦)(+πβπΎ){π§}))) |
74 | 57, 70, 72, 73 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβ(π¦ βͺ {π§})) β (πβ((πβπ¦)(+πβπΎ){π§}))) |
75 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β π§ β π΄) |
76 | 46, 67, 23 | paddatclN 38415 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ (πβπ¦) β π β§ π§ β π΄) β ((πβπ¦)(+πβπΎ){π§}) β π) |
77 | 57, 62, 75, 76 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β ((πβπ¦)(+πβπΎ){π§}) β π) |
78 | 47, 23 | psubclsubN 38406 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ ((πβπ¦)(+πβπΎ){π§}) β π) β ((πβπ¦)(+πβπΎ){π§}) β (PSubSpβπΎ)) |
79 | 57, 77, 78 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β ((πβπ¦)(+πβπΎ){π§}) β (PSubSpβπΎ)) |
80 | 47, 21 | pclidN 38362 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ ((πβπ¦)(+πβπΎ){π§}) β (PSubSpβπΎ)) β (πβ((πβπ¦)(+πβπΎ){π§})) = ((πβπ¦)(+πβπΎ){π§})) |
81 | 57, 79, 80 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβ((πβπ¦)(+πβπΎ){π§})) = ((πβπ¦)(+πβπΎ){π§})) |
82 | 74, 81 | sseqtrd 3985 |
. . . . . . . . . . . 12
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβ(π¦ βͺ {π§})) β ((πβπ¦)(+πβπΎ){π§})) |
83 | 57 | hllatd 37829 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β πΎ β Lat) |
84 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β π¦ β β
) |
85 | 46, 21 | pcl0bN 38389 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΎ β HL β§ π¦ β π΄) β ((πβπ¦) = β
β π¦ = β
)) |
86 | 85 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β ((πβπ¦) = β
β π¦ = β
)) |
87 | 86 | necon3bid 2989 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β ((πβπ¦) β β
β π¦ β β
)) |
88 | 84, 87 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβπ¦) β β
) |
89 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(leβπΎ) =
(leβπΎ) |
90 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(joinβπΎ) =
(joinβπΎ) |
91 | 89, 90, 46, 67 | elpaddat 38270 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β Lat β§ (πβπ¦) β π΄ β§ π§ β π΄) β§ (πβπ¦) β β
) β (π β ((πβπ¦)(+πβπΎ){π§}) β (π β π΄ β§ βπ β (πβπ¦)π(leβπΎ)(π(joinβπΎ)π§)))) |
92 | 83, 64, 75, 88, 91 | syl31anc 1374 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π β ((πβπ¦)(+πβπΎ){π§}) β (π β π΄ β§ βπ β (πβπ¦)π(leβπΎ)(π(joinβπΎ)π§)))) |
93 | | simp1rl 1239 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β πΎ β HL) |
94 | 93 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β πΎ β HL) |
95 | 94 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β§ (π€ β (PSubSpβπΎ) β§ (π¦ βͺ {π§}) β π€)) β πΎ β HL) |
96 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β§ (π€ β (PSubSpβπΎ) β§ (π¦ βͺ {π§}) β π€)) β π€ β (PSubSpβπΎ)) |
97 | | simpl13 1251 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β§ (π€ β (PSubSpβπΎ) β§ (π¦ βͺ {π§}) β π€)) β π β π΄) |
98 | | unss 4145 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β π€ β§ {π§} β π€) β (π¦ βͺ {π§}) β π€) |
99 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β π€ β§ {π§} β π€) β π¦ β π€) |
100 | 98, 99 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ βͺ {π§}) β π€ β π¦ β π€) |
101 | 100 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β§ (π€ β (PSubSpβπΎ) β§ (π¦ βͺ {π§}) β π€)) β π¦ β π€) |
102 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β§ (π€ β (PSubSpβπΎ) β§ (π¦ βͺ {π§}) β π€)) β π β (πβπ¦)) |
103 | 47, 21 | elpcliN 38359 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΎ β HL β§ π¦ β π€ β§ π€ β (PSubSpβπΎ)) β§ π β (πβπ¦)) β π β π€) |
104 | 95, 101, 96, 102, 103 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β§ (π€ β (PSubSpβπΎ) β§ (π¦ βͺ {π§}) β π€)) β π β π€) |
105 | 28 | snss 4747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ β π€ β {π§} β π€) |
106 | 105 | biimpri 227 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ({π§} β π€ β π§ β π€) |
107 | 106 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ β π€ β§ {π§} β π€) β π§ β π€) |
108 | 98, 107 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ βͺ {π§}) β π€ β π§ β π€) |
109 | 108 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β§ (π€ β (PSubSpβπΎ) β§ (π¦ βͺ {π§}) β π€)) β π§ β π€) |
110 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β§ (π€ β (PSubSpβπΎ) β§ (π¦ βͺ {π§}) β π€)) β π(leβπΎ)(π(joinβπΎ)π§)) |
111 | 89, 90, 46, 47 | psubspi2N 38214 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΎ β HL β§ π€ β (PSubSpβπΎ) β§ π β π΄) β§ (π β π€ β§ π§ β π€ β§ π(leβπΎ)(π(joinβπΎ)π§))) β π β π€) |
112 | 95, 96, 97, 104, 109, 110, 111 | syl33anc 1386 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π¦ β Fin
β§ π¦ β β
) β§
(πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β§ π β (πβπ¦) β§ π(leβπΎ)(π(joinβπΎ)π§)) β§ (π€ β (PSubSpβπΎ) β§ (π¦ βͺ {π§}) β π€)) β π β π€) |
113 | 112 | exp520 1358 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β (π β (πβπ¦) β (π(leβπΎ)(π(joinβπΎ)π§) β (π€ β (PSubSpβπΎ) β ((π¦ βͺ {π§}) β π€ β π β π€))))) |
114 | 113 | rexlimdv 3151 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄) β§ π β π΄) β (βπ β (πβπ¦)π(leβπΎ)(π(joinβπΎ)π§) β (π€ β (PSubSpβπΎ) β ((π¦ βͺ {π§}) β π€ β π β π€)))) |
115 | 114 | 3expia 1122 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π β π΄ β (βπ β (πβπ¦)π(leβπΎ)(π(joinβπΎ)π§) β (π€ β (PSubSpβπΎ) β ((π¦ βͺ {π§}) β π€ β π β π€))))) |
116 | 115 | impd 412 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β ((π β π΄ β§ βπ β (πβπ¦)π(leβπΎ)(π(joinβπΎ)π§)) β (π€ β (PSubSpβπΎ) β ((π¦ βͺ {π§}) β π€ β π β π€)))) |
117 | 92, 116 | sylbid 239 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π β ((πβπ¦)(+πβπΎ){π§}) β (π€ β (PSubSpβπΎ) β ((π¦ βͺ {π§}) β π€ β π β π€)))) |
118 | 117 | ralrimdv 3150 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π β ((πβπ¦)(+πβπΎ){π§}) β βπ€ β (PSubSpβπΎ)((π¦ βͺ {π§}) β π€ β π β π€))) |
119 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β π¦ β π΄) |
120 | 119, 75 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π¦ β π΄ β§ π§ β π΄)) |
121 | 120, 32 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π¦ βͺ {π§}) β π΄) |
122 | | vex 3450 |
. . . . . . . . . . . . . . . 16
β’ π β V |
123 | 46, 47, 21, 122 | elpclN 38358 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ (π¦ βͺ {π§}) β π΄) β (π β (πβ(π¦ βͺ {π§})) β βπ€ β (PSubSpβπΎ)((π¦ βͺ {π§}) β π€ β π β π€))) |
124 | 57, 121, 123 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π β (πβ(π¦ βͺ {π§})) β βπ€ β (PSubSpβπΎ)((π¦ βͺ {π§}) β π€ β π β π€))) |
125 | 118, 124 | sylibrd 259 |
. . . . . . . . . . . . 13
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (π β ((πβπ¦)(+πβπΎ){π§}) β π β (πβ(π¦ βͺ {π§})))) |
126 | 125 | ssrdv 3951 |
. . . . . . . . . . . 12
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β ((πβπ¦)(+πβπΎ){π§}) β (πβ(π¦ βͺ {π§}))) |
127 | 82, 126 | eqssd 3962 |
. . . . . . . . . . 11
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβ(π¦ βͺ {π§})) = ((πβπ¦)(+πβπΎ){π§})) |
128 | 127, 77 | eqeltrd 2838 |
. . . . . . . . . 10
β’ ((((π¦ β Fin β§ π¦ β β
) β§ (πΎ β HL β§ π¦ β π΄)) β§ ((πβπ¦) β π β§ π§ β π΄)) β (πβ(π¦ βͺ {π§})) β π) |
129 | 128 | exp43 438 |
. . . . . . . . 9
β’ ((π¦ β Fin β§ π¦ β β
) β ((πΎ β HL β§ π¦ β π΄) β ((πβπ¦) β π β (π§ β π΄ β (πβ(π¦ βͺ {π§})) β π)))) |
130 | 56, 129 | pm2.61dane 3033 |
. . . . . . . 8
β’ (π¦ β Fin β ((πΎ β HL β§ π¦ β π΄) β ((πβπ¦) β π β (π§ β π΄ β (πβ(π¦ βͺ {π§})) β π)))) |
131 | 130 | a2d 29 |
. . . . . . 7
β’ (π¦ β Fin β (((πΎ β HL β§ π¦ β π΄) β (πβπ¦) β π) β ((πΎ β HL β§ π¦ β π΄) β (π§ β π΄ β (πβ(π¦ βͺ {π§})) β π)))) |
132 | 131 | imp4b 423 |
. . . . . 6
β’ ((π¦ β Fin β§ ((πΎ β HL β§ π¦ β π΄) β (πβπ¦) β π)) β (((πΎ β HL β§ π¦ β π΄) β§ π§ β π΄) β (πβ(π¦ βͺ {π§})) β π)) |
133 | 34, 132 | biimtrid 241 |
. . . . 5
β’ ((π¦ β Fin β§ ((πΎ β HL β§ π¦ β π΄) β (πβπ¦) β π)) β ((πΎ β HL β§ (π¦ βͺ {π§}) β π΄) β (πβ(π¦ βͺ {π§})) β π)) |
134 | 133 | ex 414 |
. . . 4
β’ (π¦ β Fin β (((πΎ β HL β§ π¦ β π΄) β (πβπ¦) β π) β ((πΎ β HL β§ (π¦ βͺ {π§}) β π΄) β (πβ(π¦ βͺ {π§})) β π))) |
135 | 5, 10, 15, 20, 26, 134 | findcard2 9109 |
. . 3
β’ (π β Fin β ((πΎ β HL β§ π β π΄) β (πβπ) β π)) |
136 | 135 | 3impib 1117 |
. 2
β’ ((π β Fin β§ πΎ β HL β§ π β π΄) β (πβπ) β π) |
137 | 136 | 3coml 1128 |
1
β’ ((πΎ β HL β§ π β π΄ β§ π β Fin) β (πβπ) β π) |