Step | Hyp | Ref
| Expression |
1 | | f1f 6743 |
. . . . . . 7
β’ (πΉ:(0..^(β―βπΉ))β1-1βdom πΈ β πΉ:(0..^(β―βπΉ))βΆdom πΈ) |
2 | 1 | frnd 6681 |
. . . . . 6
β’ (πΉ:(0..^(β―βπΉ))β1-1βdom πΈ β ran πΉ β dom πΈ) |
3 | 2 | adantl 483 |
. . . . 5
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β ran πΉ β dom πΈ) |
4 | | ssdmres 5965 |
. . . . 5
β’ (ran
πΉ β dom πΈ β dom (πΈ βΎ ran πΉ) = ran πΉ) |
5 | 3, 4 | sylib 217 |
. . . 4
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β dom (πΈ βΎ ran πΉ) = ran πΉ) |
6 | 5 | fveq2d 6851 |
. . 3
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (β―βdom (πΈ βΎ ran πΉ)) = (β―βran πΉ)) |
7 | | df-ima 5651 |
. . . . 5
β’ (πΈ β ran πΉ) = ran (πΈ βΎ ran πΉ) |
8 | 7 | fveq2i 6850 |
. . . 4
β’
(β―β(πΈ
β ran πΉ)) =
(β―βran (πΈ
βΎ ran πΉ)) |
9 | | f1fun 6745 |
. . . . . . . 8
β’ (πΈ:dom πΈβ1-1βran πΈ β Fun πΈ) |
10 | | funres 6548 |
. . . . . . . . 9
β’ (Fun
πΈ β Fun (πΈ βΎ ran πΉ)) |
11 | 10 | funfnd 6537 |
. . . . . . . 8
β’ (Fun
πΈ β (πΈ βΎ ran πΉ) Fn dom (πΈ βΎ ran πΉ)) |
12 | 9, 11 | syl 17 |
. . . . . . 7
β’ (πΈ:dom πΈβ1-1βran πΈ β (πΈ βΎ ran πΉ) Fn dom (πΈ βΎ ran πΉ)) |
13 | 12 | ad2antrr 725 |
. . . . . 6
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (πΈ βΎ ran πΉ) Fn dom (πΈ βΎ ran πΉ)) |
14 | | hashfn 14282 |
. . . . . 6
β’ ((πΈ βΎ ran πΉ) Fn dom (πΈ βΎ ran πΉ) β (β―β(πΈ βΎ ran πΉ)) = (β―βdom (πΈ βΎ ran πΉ))) |
15 | 13, 14 | syl 17 |
. . . . 5
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (β―β(πΈ βΎ ran πΉ)) = (β―βdom (πΈ βΎ ran πΉ))) |
16 | | ovex 7395 |
. . . . . . . 8
β’
(0..^(β―βπΉ)) β V |
17 | | fex 7181 |
. . . . . . . 8
β’ ((πΉ:(0..^(β―βπΉ))βΆdom πΈ β§ (0..^(β―βπΉ)) β V) β πΉ β V) |
18 | 1, 16, 17 | sylancl 587 |
. . . . . . 7
β’ (πΉ:(0..^(β―βπΉ))β1-1βdom πΈ β πΉ β V) |
19 | | rnexg 7846 |
. . . . . . 7
β’ (πΉ β V β ran πΉ β V) |
20 | 18, 19 | syl 17 |
. . . . . 6
β’ (πΉ:(0..^(β―βπΉ))β1-1βdom πΈ β ran πΉ β V) |
21 | | simpll 766 |
. . . . . . 7
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β πΈ:dom πΈβ1-1βran πΈ) |
22 | | f1ssres 6751 |
. . . . . . 7
β’ ((πΈ:dom πΈβ1-1βran πΈ β§ ran πΉ β dom πΈ) β (πΈ βΎ ran πΉ):ran πΉβ1-1βran πΈ) |
23 | 21, 3, 22 | syl2anc 585 |
. . . . . 6
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (πΈ βΎ ran πΉ):ran πΉβ1-1βran πΈ) |
24 | | hashf1rn 14259 |
. . . . . 6
β’ ((ran
πΉ β V β§ (πΈ βΎ ran πΉ):ran πΉβ1-1βran πΈ) β (β―β(πΈ βΎ ran πΉ)) = (β―βran (πΈ βΎ ran πΉ))) |
25 | 20, 23, 24 | syl2an2 685 |
. . . . 5
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (β―β(πΈ βΎ ran πΉ)) = (β―βran (πΈ βΎ ran πΉ))) |
26 | 15, 25 | eqtr3d 2779 |
. . . 4
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (β―βdom (πΈ βΎ ran πΉ)) = (β―βran (πΈ βΎ ran πΉ))) |
27 | 8, 26 | eqtr4id 2796 |
. . 3
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (β―β(πΈ β ran πΉ)) = (β―βdom (πΈ βΎ ran πΉ))) |
28 | | hashf1rn 14259 |
. . . . 5
β’
(((0..^(β―βπΉ)) β V β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (β―βπΉ) = (β―βran πΉ)) |
29 | 16, 28 | mpan 689 |
. . . 4
β’ (πΉ:(0..^(β―βπΉ))β1-1βdom πΈ β (β―βπΉ) = (β―βran πΉ)) |
30 | 29 | adantl 483 |
. . 3
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (β―βπΉ) = (β―βran πΉ)) |
31 | 6, 27, 30 | 3eqtr4d 2787 |
. 2
β’ (((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β§ πΉ:(0..^(β―βπΉ))β1-1βdom πΈ) β (β―β(πΈ β ran πΉ)) = (β―βπΉ)) |
32 | 31 | ex 414 |
1
β’ ((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β (πΉ:(0..^(β―βπΉ))β1-1βdom πΈ β (β―β(πΈ β ran πΉ)) = (β―βπΉ))) |