Step | Hyp | Ref
| Expression |
1 | | lshpset.v |
. . . 4
β’ π = (Baseβπ) |
2 | | lshpset.n |
. . . 4
β’ π = (LSpanβπ) |
3 | | lshpset.s |
. . . 4
β’ π = (LSubSpβπ) |
4 | | lshpset.h |
. . . 4
β’ π» = (LSHypβπ) |
5 | 1, 2, 3, 4 | lshpset 37469 |
. . 3
β’ (π β π β π» = {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)}) |
6 | 5 | eleq2d 2824 |
. 2
β’ (π β π β (π β π» β π β {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)})) |
7 | | neeq1 3007 |
. . . . 5
β’ (π = π β (π β π β π β π)) |
8 | | uneq1 4121 |
. . . . . . 7
β’ (π = π β (π βͺ {π£}) = (π βͺ {π£})) |
9 | 8 | fveqeq2d 6855 |
. . . . . 6
β’ (π = π β ((πβ(π βͺ {π£})) = π β (πβ(π βͺ {π£})) = π)) |
10 | 9 | rexbidv 3176 |
. . . . 5
β’ (π = π β (βπ£ β π (πβ(π βͺ {π£})) = π β βπ£ β π (πβ(π βͺ {π£})) = π)) |
11 | 7, 10 | anbi12d 632 |
. . . 4
β’ (π = π β ((π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π) β (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
12 | 11 | elrab 3650 |
. . 3
β’ (π β {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)} β (π β π β§ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
13 | | 3anass 1096 |
. . 3
β’ ((π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π) β (π β π β§ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
14 | 12, 13 | bitr4i 278 |
. 2
β’ (π β {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)} β (π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)) |
15 | 6, 14 | bitrdi 287 |
1
β’ (π β π β (π β π» β (π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |