Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. 2
β’ (πΎ β π΅ β πΎ β V) |
2 | | lineset.n |
. . 3
β’ π = (LinesβπΎ) |
3 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
4 | | lineset.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΎ β (Atomsβπ) = π΄) |
6 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
7 | | lineset.l |
. . . . . . . . . . . . 13
β’ β€ =
(leβπΎ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (π = πΎ β (leβπ) = β€ ) |
9 | 8 | breqd 5120 |
. . . . . . . . . . 11
β’ (π = πΎ β (π(leβπ)(π(joinβπ)π) β π β€ (π(joinβπ)π))) |
10 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
11 | | lineset.j |
. . . . . . . . . . . . . 14
β’ β¨ =
(joinβπΎ) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ (π = πΎ β (joinβπ) = β¨ ) |
13 | 12 | oveqd 7378 |
. . . . . . . . . . . 12
β’ (π = πΎ β (π(joinβπ)π) = (π β¨ π)) |
14 | 13 | breq2d 5121 |
. . . . . . . . . . 11
β’ (π = πΎ β (π β€ (π(joinβπ)π) β π β€ (π β¨ π))) |
15 | 9, 14 | bitrd 279 |
. . . . . . . . . 10
β’ (π = πΎ β (π(leβπ)(π(joinβπ)π) β π β€ (π β¨ π))) |
16 | 5, 15 | rabeqbidv 3423 |
. . . . . . . . 9
β’ (π = πΎ β {π β (Atomsβπ) β£ π(leβπ)(π(joinβπ)π)} = {π β π΄ β£ π β€ (π β¨ π)}) |
17 | 16 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = πΎ β (π = {π β (Atomsβπ) β£ π(leβπ)(π(joinβπ)π)} β π = {π β π΄ β£ π β€ (π β¨ π)})) |
18 | 17 | anbi2d 630 |
. . . . . . 7
β’ (π = πΎ β ((π β π β§ π = {π β (Atomsβπ) β£ π(leβπ)(π(joinβπ)π)}) β (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)}))) |
19 | 5, 18 | rexeqbidv 3319 |
. . . . . 6
β’ (π = πΎ β (βπ β (Atomsβπ)(π β π β§ π = {π β (Atomsβπ) β£ π(leβπ)(π(joinβπ)π)}) β βπ β π΄ (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)}))) |
20 | 5, 19 | rexeqbidv 3319 |
. . . . 5
β’ (π = πΎ β (βπ β (Atomsβπ)βπ β (Atomsβπ)(π β π β§ π = {π β (Atomsβπ) β£ π(leβπ)(π(joinβπ)π)}) β βπ β π΄ βπ β π΄ (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)}))) |
21 | 20 | abbidv 2802 |
. . . 4
β’ (π = πΎ β {π β£ βπ β (Atomsβπ)βπ β (Atomsβπ)(π β π β§ π = {π β (Atomsβπ) β£ π(leβπ)(π(joinβπ)π)})} = {π β£ βπ β π΄ βπ β π΄ (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)})}) |
22 | | df-lines 38014 |
. . . 4
β’ Lines =
(π β V β¦ {π β£ βπ β (Atomsβπ)βπ β (Atomsβπ)(π β π β§ π = {π β (Atomsβπ) β£ π(leβπ)(π(joinβπ)π)})}) |
23 | 4 | fvexi 6860 |
. . . . 5
β’ π΄ β V |
24 | | df-sn 4591 |
. . . . . . 7
β’ {{π β π΄ β£ π β€ (π β¨ π)}} = {π β£ π = {π β π΄ β£ π β€ (π β¨ π)}} |
25 | | snex 5392 |
. . . . . . 7
β’ {{π β π΄ β£ π β€ (π β¨ π)}} β V |
26 | 24, 25 | eqeltrri 2831 |
. . . . . 6
β’ {π β£ π = {π β π΄ β£ π β€ (π β¨ π)}} β V |
27 | | simpr 486 |
. . . . . . 7
β’ ((π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)}) β π = {π β π΄ β£ π β€ (π β¨ π)}) |
28 | 27 | ss2abi 4027 |
. . . . . 6
β’ {π β£ (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)})} β {π β£ π = {π β π΄ β£ π β€ (π β¨ π)}} |
29 | 26, 28 | ssexi 5283 |
. . . . 5
β’ {π β£ (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)})} β V |
30 | 23, 23, 29 | ab2rexex2 7917 |
. . . 4
β’ {π β£ βπ β π΄ βπ β π΄ (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)})} β V |
31 | 21, 22, 30 | fvmpt 6952 |
. . 3
β’ (πΎ β V β
(LinesβπΎ) = {π β£ βπ β π΄ βπ β π΄ (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)})}) |
32 | 2, 31 | eqtrid 2785 |
. 2
β’ (πΎ β V β π = {π β£ βπ β π΄ βπ β π΄ (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)})}) |
33 | 1, 32 | syl 17 |
1
β’ (πΎ β π΅ β π = {π β£ βπ β π΄ βπ β π΄ (π β π β§ π = {π β π΄ β£ π β€ (π β¨ π)})}) |