Step | Hyp | Ref
| Expression |
1 | | lshpset.h |
. 2
β’ π» = (LSHypβπ) |
2 | | elex 3466 |
. . 3
β’ (π β π β π β V) |
3 | | fveq2 6847 |
. . . . . 6
β’ (π€ = π β (LSubSpβπ€) = (LSubSpβπ)) |
4 | | lshpset.s |
. . . . . 6
β’ π = (LSubSpβπ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
β’ (π€ = π β (LSubSpβπ€) = π) |
6 | | fveq2 6847 |
. . . . . . . 8
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
7 | | lshpset.v |
. . . . . . . 8
β’ π = (Baseβπ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β (Baseβπ€) = π) |
9 | 8 | neeq2d 3005 |
. . . . . 6
β’ (π€ = π β (π β (Baseβπ€) β π β π)) |
10 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π€ = π β (LSpanβπ€) = (LSpanβπ)) |
11 | | lshpset.n |
. . . . . . . . . 10
β’ π = (LSpanβπ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π€ = π β (LSpanβπ€) = π) |
13 | 12 | fveq1d 6849 |
. . . . . . . 8
β’ (π€ = π β ((LSpanβπ€)β(π βͺ {π£})) = (πβ(π βͺ {π£}))) |
14 | 13, 8 | eqeq12d 2753 |
. . . . . . 7
β’ (π€ = π β (((LSpanβπ€)β(π βͺ {π£})) = (Baseβπ€) β (πβ(π βͺ {π£})) = π)) |
15 | 8, 14 | rexeqbidv 3323 |
. . . . . 6
β’ (π€ = π β (βπ£ β (Baseβπ€)((LSpanβπ€)β(π βͺ {π£})) = (Baseβπ€) β βπ£ β π (πβ(π βͺ {π£})) = π)) |
16 | 9, 15 | anbi12d 632 |
. . . . 5
β’ (π€ = π β ((π β (Baseβπ€) β§ βπ£ β (Baseβπ€)((LSpanβπ€)β(π βͺ {π£})) = (Baseβπ€)) β (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) |
17 | 5, 16 | rabeqbidv 3427 |
. . . 4
β’ (π€ = π β {π β (LSubSpβπ€) β£ (π β (Baseβπ€) β§ βπ£ β (Baseβπ€)((LSpanβπ€)β(π βͺ {π£})) = (Baseβπ€))} = {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)}) |
18 | | df-lshyp 37468 |
. . . 4
β’ LSHyp =
(π€ β V β¦ {π β (LSubSpβπ€) β£ (π β (Baseβπ€) β§ βπ£ β (Baseβπ€)((LSpanβπ€)β(π βͺ {π£})) = (Baseβπ€))}) |
19 | 4 | fvexi 6861 |
. . . . 5
β’ π β V |
20 | 19 | rabex 5294 |
. . . 4
β’ {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)} β V |
21 | 17, 18, 20 | fvmpt 6953 |
. . 3
β’ (π β V β
(LSHypβπ) = {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)}) |
22 | 2, 21 | syl 17 |
. 2
β’ (π β π β (LSHypβπ) = {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)}) |
23 | 1, 22 | eqtrid 2789 |
1
β’ (π β π β π» = {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)}) |