Step | Hyp | Ref
| Expression |
1 | | dvf 25424 |
. . 3
β’ (β
D πΉ):dom (β D πΉ)βΆβ |
2 | | ffn 6718 |
. . 3
β’ ((β
D πΉ):dom (β D πΉ)βΆβ β (β
D πΉ) Fn dom (β D
πΉ)) |
3 | 1, 2 | mp1i 13 |
. 2
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β D πΉ) Fn dom (β D πΉ)) |
4 | 1 | ffvelcdmi 7086 |
. . . . 5
β’ (π₯ β dom (β D πΉ) β ((β D πΉ)βπ₯) β β) |
5 | 4 | adantl 483 |
. . . 4
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π₯ β dom (β D πΉ)) β ((β D πΉ)βπ₯) β β) |
6 | | simpr 486 |
. . . . . 6
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π₯ β dom (β D πΉ)) β π₯ β dom (β D πΉ)) |
7 | | fvco3 6991 |
. . . . . 6
β’
(((β D πΉ):dom
(β D πΉ)βΆβ β§ π₯ β dom (β D πΉ)) β ((β β (β D
πΉ))βπ₯) = (ββ((β D
πΉ)βπ₯))) |
8 | 1, 6, 7 | sylancr 588 |
. . . . 5
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π₯ β dom (β D πΉ)) β ((β β (β D
πΉ))βπ₯) = (ββ((β D
πΉ)βπ₯))) |
9 | | ax-resscn 11167 |
. . . . . . . . . 10
β’ β
β β |
10 | | fss 6735 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ β β
β) β πΉ:π΄βΆβ) |
11 | 9, 10 | mpan2 690 |
. . . . . . . . 9
β’ (πΉ:π΄βΆβ β πΉ:π΄βΆβ) |
12 | | dvcj 25467 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β D
(β β πΉ)) =
(β β (β D πΉ))) |
13 | 11, 12 | sylan 581 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β D
(β β πΉ)) =
(β β (β D πΉ))) |
14 | | ffvelcdm 7084 |
. . . . . . . . . . . . 13
β’ ((πΉ:π΄βΆβ β§ π¦ β π΄) β (πΉβπ¦) β β) |
15 | 14 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π¦ β π΄) β (πΉβπ¦) β β) |
16 | 15 | cjred 15173 |
. . . . . . . . . . 11
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π¦ β π΄) β (ββ(πΉβπ¦)) = (πΉβπ¦)) |
17 | 16 | mpteq2dva 5249 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (π¦ β π΄ β¦ (ββ(πΉβπ¦))) = (π¦ β π΄ β¦ (πΉβπ¦))) |
18 | 15 | recnd 11242 |
. . . . . . . . . . 11
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π¦ β π΄) β (πΉβπ¦) β β) |
19 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ:π΄βΆβ) |
20 | 19 | feqmptd 6961 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ = (π¦ β π΄ β¦ (πΉβπ¦))) |
21 | | cjf 15051 |
. . . . . . . . . . . . 13
β’
β:ββΆβ |
22 | 21 | a1i 11 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β
β:ββΆβ) |
23 | 22 | feqmptd 6961 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β β = (π§ β β β¦
(ββπ§))) |
24 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π§ = (πΉβπ¦) β (ββπ§) = (ββ(πΉβπ¦))) |
25 | 18, 20, 23, 24 | fmptco 7127 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β β
πΉ) = (π¦ β π΄ β¦ (ββ(πΉβπ¦)))) |
26 | 17, 25, 20 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β β
πΉ) = πΉ) |
27 | 26 | oveq2d 7425 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β D
(β β πΉ)) =
(β D πΉ)) |
28 | 13, 27 | eqtr3d 2775 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β β
(β D πΉ)) = (β D
πΉ)) |
29 | 28 | fveq1d 6894 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β ((β β
(β D πΉ))βπ₯) = ((β D πΉ)βπ₯)) |
30 | 29 | adantr 482 |
. . . . 5
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π₯ β dom (β D πΉ)) β ((β β (β D
πΉ))βπ₯) = ((β D πΉ)βπ₯)) |
31 | 8, 30 | eqtr3d 2775 |
. . . 4
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π₯ β dom (β D πΉ)) β (ββ((β D πΉ)βπ₯)) = ((β D πΉ)βπ₯)) |
32 | 5, 31 | cjrebd 15149 |
. . 3
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π₯ β dom (β D πΉ)) β ((β D πΉ)βπ₯) β β) |
33 | 32 | ralrimiva 3147 |
. 2
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β βπ₯ β dom (β D πΉ)((β D πΉ)βπ₯) β β) |
34 | | ffnfv 7118 |
. 2
β’ ((β
D πΉ):dom (β D πΉ)βΆβ β
((β D πΉ) Fn dom
(β D πΉ) β§
βπ₯ β dom
(β D πΉ)((β D
πΉ)βπ₯) β β)) |
35 | 3, 33, 34 | sylanbrc 584 |
1
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β D πΉ):dom (β D πΉ)βΆβ) |