Step | Hyp | Ref
| Expression |
1 | | ldilset.d |
. 2
β’ π· = ((LDilβπΎ)βπ) |
2 | | ldilset.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | ldilset.l |
. . . . 5
β’ β€ =
(leβπΎ) |
4 | | ldilset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | | ldilset.i |
. . . . 5
β’ πΌ = (LAutβπΎ) |
6 | 2, 3, 4, 5 | ldilfset 38600 |
. . . 4
β’ (πΎ β πΆ β (LDilβπΎ) = (π€ β π» β¦ {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π€ β (πβπ₯) = π₯)})) |
7 | 6 | fveq1d 6849 |
. . 3
β’ (πΎ β πΆ β ((LDilβπΎ)βπ) = ((π€ β π» β¦ {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π€ β (πβπ₯) = π₯)})βπ)) |
8 | | breq2 5114 |
. . . . . . 7
β’ (π€ = π β (π₯ β€ π€ β π₯ β€ π)) |
9 | 8 | imbi1d 342 |
. . . . . 6
β’ (π€ = π β ((π₯ β€ π€ β (πβπ₯) = π₯) β (π₯ β€ π β (πβπ₯) = π₯))) |
10 | 9 | ralbidv 3175 |
. . . . 5
β’ (π€ = π β (βπ₯ β π΅ (π₯ β€ π€ β (πβπ₯) = π₯) β βπ₯ β π΅ (π₯ β€ π β (πβπ₯) = π₯))) |
11 | 10 | rabbidv 3418 |
. . . 4
β’ (π€ = π β {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π€ β (πβπ₯) = π₯)} = {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π β (πβπ₯) = π₯)}) |
12 | | eqid 2737 |
. . . 4
β’ (π€ β π» β¦ {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π€ β (πβπ₯) = π₯)}) = (π€ β π» β¦ {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π€ β (πβπ₯) = π₯)}) |
13 | 5 | fvexi 6861 |
. . . . 5
β’ πΌ β V |
14 | 13 | rabex 5294 |
. . . 4
β’ {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π β (πβπ₯) = π₯)} β V |
15 | 11, 12, 14 | fvmpt 6953 |
. . 3
β’ (π β π» β ((π€ β π» β¦ {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π€ β (πβπ₯) = π₯)})βπ) = {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π β (πβπ₯) = π₯)}) |
16 | 7, 15 | sylan9eq 2797 |
. 2
β’ ((πΎ β πΆ β§ π β π») β ((LDilβπΎ)βπ) = {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π β (πβπ₯) = π₯)}) |
17 | 1, 16 | eqtrid 2789 |
1
β’ ((πΎ β πΆ β§ π β π») β π· = {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π β (πβπ₯) = π₯)}) |