Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | eqid 2737 |
. . . 4
β’
(leβπΎ) =
(leβπΎ) |
3 | | dibcl.h |
. . . 4
β’ π» = (LHypβπΎ) |
4 | | dibcl.i |
. . . 4
β’ πΌ = ((DIsoBβπΎ)βπ) |
5 | 1, 2, 3, 4 | dibfnN 39622 |
. . 3
β’ ((πΎ β HL β§ π β π») β πΌ Fn {π₯ β (BaseβπΎ) β£ π₯(leβπΎ)π}) |
6 | | fnfun 6603 |
. . . 4
β’ (πΌ Fn {π₯ β (BaseβπΎ) β£ π₯(leβπΎ)π} β Fun πΌ) |
7 | | funfn 6532 |
. . . 4
β’ (Fun
πΌ β πΌ Fn dom πΌ) |
8 | 6, 7 | sylib 217 |
. . 3
β’ (πΌ Fn {π₯ β (BaseβπΎ) β£ π₯(leβπΎ)π} β πΌ Fn dom πΌ) |
9 | 5, 8 | syl 17 |
. 2
β’ ((πΎ β HL β§ π β π») β πΌ Fn dom πΌ) |
10 | | eqidd 2738 |
. 2
β’ ((πΎ β HL β§ π β π») β ran πΌ = ran πΌ) |
11 | 1, 2, 3, 4 | dibeldmN 39624 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π₯ β dom πΌ β (π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π))) |
12 | 1, 2, 3, 4 | dibeldmN 39624 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π¦ β dom πΌ β (π¦ β (BaseβπΎ) β§ π¦(leβπΎ)π))) |
13 | 11, 12 | anbi12d 632 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ((π₯ β dom πΌ β§ π¦ β dom πΌ) β ((π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π) β§ (π¦ β (BaseβπΎ) β§ π¦(leβπΎ)π)))) |
14 | 1, 2, 3, 4 | dib11N 39626 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π) β§ (π¦ β (BaseβπΎ) β§ π¦(leβπΎ)π)) β ((πΌβπ₯) = (πΌβπ¦) β π₯ = π¦)) |
15 | 14 | biimpd 228 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π) β§ (π¦ β (BaseβπΎ) β§ π¦(leβπΎ)π)) β ((πΌβπ₯) = (πΌβπ¦) β π₯ = π¦)) |
16 | 15 | 3expib 1123 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (((π₯ β (BaseβπΎ) β§ π₯(leβπΎ)π) β§ (π¦ β (BaseβπΎ) β§ π¦(leβπΎ)π)) β ((πΌβπ₯) = (πΌβπ¦) β π₯ = π¦))) |
17 | 13, 16 | sylbid 239 |
. . 3
β’ ((πΎ β HL β§ π β π») β ((π₯ β dom πΌ β§ π¦ β dom πΌ) β ((πΌβπ₯) = (πΌβπ¦) β π₯ = π¦))) |
18 | 17 | ralrimivv 3196 |
. 2
β’ ((πΎ β HL β§ π β π») β βπ₯ β dom πΌβπ¦ β dom πΌ((πΌβπ₯) = (πΌβπ¦) β π₯ = π¦)) |
19 | | dff1o6 7222 |
. 2
β’ (πΌ:dom πΌβ1-1-ontoβran
πΌ β (πΌ Fn dom πΌ β§ ran πΌ = ran πΌ β§ βπ₯ β dom πΌβπ¦ β dom πΌ((πΌβπ₯) = (πΌβπ¦) β π₯ = π¦))) |
20 | 9, 10, 18, 19 | syl3anbrc 1344 |
1
β’ ((πΎ β HL β§ π β π») β πΌ:dom πΌβ1-1-ontoβran
πΌ) |