Step | Hyp | Ref
| Expression |
1 | | elex 3466 |
. 2
β’ (πΎ β π· β πΎ β V) |
2 | | llnset.n |
. . 3
β’ π = (LLinesβπΎ) |
3 | | fveq2 6847 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
4 | | llnset.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
β’ (π = πΎ β (Baseβπ) = π΅) |
6 | | fveq2 6847 |
. . . . . . 7
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
7 | | llnset.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . 6
β’ (π = πΎ β (Atomsβπ) = π΄) |
9 | | fveq2 6847 |
. . . . . . . 8
β’ (π = πΎ β ( β βπ) = ( β βπΎ)) |
10 | | llnset.c |
. . . . . . . 8
β’ πΆ = ( β βπΎ) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β ( β βπ) = πΆ) |
12 | 11 | breqd 5121 |
. . . . . 6
β’ (π = πΎ β (π( β βπ)π₯ β ππΆπ₯)) |
13 | 8, 12 | rexeqbidv 3323 |
. . . . 5
β’ (π = πΎ β (βπ β (Atomsβπ)π( β βπ)π₯ β βπ β π΄ ππΆπ₯)) |
14 | 5, 13 | rabeqbidv 3427 |
. . . 4
β’ (π = πΎ β {π₯ β (Baseβπ) β£ βπ β (Atomsβπ)π( β βπ)π₯} = {π₯ β π΅ β£ βπ β π΄ ππΆπ₯}) |
15 | | df-llines 37990 |
. . . 4
β’ LLines =
(π β V β¦ {π₯ β (Baseβπ) β£ βπ β (Atomsβπ)π( β βπ)π₯}) |
16 | 4 | fvexi 6861 |
. . . . 5
β’ π΅ β V |
17 | 16 | rabex 5294 |
. . . 4
β’ {π₯ β π΅ β£ βπ β π΄ ππΆπ₯} β V |
18 | 14, 15, 17 | fvmpt 6953 |
. . 3
β’ (πΎ β V β
(LLinesβπΎ) = {π₯ β π΅ β£ βπ β π΄ ππΆπ₯}) |
19 | 2, 18 | eqtrid 2789 |
. 2
β’ (πΎ β V β π = {π₯ β π΅ β£ βπ β π΄ ππΆπ₯}) |
20 | 1, 19 | syl 17 |
1
β’ (πΎ β π· β π = {π₯ β π΅ β£ βπ β π΄ ππΆπ₯}) |