Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | eqid 2733 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
3 | | diaelrn.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | | diaelrn.i |
. . . . 5
β’ πΌ = ((DIsoAβπΎ)βπ) |
5 | 1, 2, 3, 4 | diafn 39547 |
. . . 4
β’ ((πΎ β π β§ π β π») β πΌ Fn {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π}) |
6 | | fvelrnb 6907 |
. . . 4
β’ (πΌ Fn {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π} β (π β ran πΌ β βπ₯ β {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π} (πΌβπ₯) = π)) |
7 | 5, 6 | syl 17 |
. . 3
β’ ((πΎ β π β§ π β π») β (π β ran πΌ β βπ₯ β {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π} (πΌβπ₯) = π)) |
8 | | breq1 5112 |
. . . . . 6
β’ (π¦ = π₯ β (π¦(leβπΎ)π β π₯(leβπΎ)π)) |
9 | 8 | elrab 3649 |
. . . . 5
β’ (π₯ β {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π} β (π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π)) |
10 | | diaelrn.t |
. . . . . . . 8
β’ π = ((LTrnβπΎ)βπ) |
11 | 1, 2, 3, 10, 4 | diass 39555 |
. . . . . . 7
β’ (((πΎ β π β§ π β π») β§ (π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π)) β (πΌβπ₯) β π) |
12 | 11 | ex 414 |
. . . . . 6
β’ ((πΎ β π β§ π β π») β ((π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π) β (πΌβπ₯) β π)) |
13 | | sseq1 3973 |
. . . . . . 7
β’ ((πΌβπ₯) = π β ((πΌβπ₯) β π β π β π)) |
14 | 13 | biimpcd 249 |
. . . . . 6
β’ ((πΌβπ₯) β π β ((πΌβπ₯) = π β π β π)) |
15 | 12, 14 | syl6 35 |
. . . . 5
β’ ((πΎ β π β§ π β π») β ((π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π) β ((πΌβπ₯) = π β π β π))) |
16 | 9, 15 | biimtrid 241 |
. . . 4
β’ ((πΎ β π β§ π β π») β (π₯ β {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π} β ((πΌβπ₯) = π β π β π))) |
17 | 16 | rexlimdv 3147 |
. . 3
β’ ((πΎ β π β§ π β π») β (βπ₯ β {π¦ β (BaseβπΎ) β£ π¦(leβπΎ)π} (πΌβπ₯) = π β π β π)) |
18 | 7, 17 | sylbid 239 |
. 2
β’ ((πΎ β π β§ π β π») β (π β ran πΌ β π β π)) |
19 | 18 | imp 408 |
1
β’ (((πΎ β π β§ π β π») β§ π β ran πΌ) β π β π) |