Step | Hyp | Ref
| Expression |
1 | | arwrcl.a |
. . . . . . 7
β’ π΄ = (ArrowβπΆ) |
2 | | arwhoma.h |
. . . . . . 7
β’ π» =
(HomaβπΆ) |
3 | 1, 2 | arwval 17997 |
. . . . . 6
β’ π΄ = βͺ
ran π» |
4 | 3 | eleq2i 2823 |
. . . . 5
β’ (πΉ β π΄ β πΉ β βͺ ran
π») |
5 | 4 | biimpi 215 |
. . . 4
β’ (πΉ β π΄ β πΉ β βͺ ran
π») |
6 | | eqid 2730 |
. . . . . 6
β’
(BaseβπΆ) =
(BaseβπΆ) |
7 | 1 | arwrcl 17998 |
. . . . . 6
β’ (πΉ β π΄ β πΆ β Cat) |
8 | 2, 6, 7 | homaf 17984 |
. . . . 5
β’ (πΉ β π΄ β π»:((BaseβπΆ) Γ (BaseβπΆ))βΆπ« (((BaseβπΆ) Γ (BaseβπΆ)) Γ V)) |
9 | | ffn 6716 |
. . . . 5
β’ (π»:((BaseβπΆ) Γ (BaseβπΆ))βΆπ« (((BaseβπΆ) Γ (BaseβπΆ)) Γ V) β π» Fn ((BaseβπΆ) Γ (BaseβπΆ))) |
10 | | fnunirn 7255 |
. . . . 5
β’ (π» Fn ((BaseβπΆ) Γ (BaseβπΆ)) β (πΉ β βͺ ran
π» β βπ§ β ((BaseβπΆ) Γ (BaseβπΆ))πΉ β (π»βπ§))) |
11 | 8, 9, 10 | 3syl 18 |
. . . 4
β’ (πΉ β π΄ β (πΉ β βͺ ran
π» β βπ§ β ((BaseβπΆ) Γ (BaseβπΆ))πΉ β (π»βπ§))) |
12 | 5, 11 | mpbid 231 |
. . 3
β’ (πΉ β π΄ β βπ§ β ((BaseβπΆ) Γ (BaseβπΆ))πΉ β (π»βπ§)) |
13 | | fveq2 6890 |
. . . . . 6
β’ (π§ = β¨π₯, π¦β© β (π»βπ§) = (π»ββ¨π₯, π¦β©)) |
14 | | df-ov 7414 |
. . . . . 6
β’ (π₯π»π¦) = (π»ββ¨π₯, π¦β©) |
15 | 13, 14 | eqtr4di 2788 |
. . . . 5
β’ (π§ = β¨π₯, π¦β© β (π»βπ§) = (π₯π»π¦)) |
16 | 15 | eleq2d 2817 |
. . . 4
β’ (π§ = β¨π₯, π¦β© β (πΉ β (π»βπ§) β πΉ β (π₯π»π¦))) |
17 | 16 | rexxp 5841 |
. . 3
β’
(βπ§ β
((BaseβπΆ) Γ
(BaseβπΆ))πΉ β (π»βπ§) β βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)πΉ β (π₯π»π¦)) |
18 | 12, 17 | sylib 217 |
. 2
β’ (πΉ β π΄ β βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)πΉ β (π₯π»π¦)) |
19 | | id 22 |
. . . . 5
β’ (πΉ β (π₯π»π¦) β πΉ β (π₯π»π¦)) |
20 | 2 | homadm 17994 |
. . . . . 6
β’ (πΉ β (π₯π»π¦) β (domaβπΉ) = π₯) |
21 | 2 | homacd 17995 |
. . . . . 6
β’ (πΉ β (π₯π»π¦) β (codaβπΉ) = π¦) |
22 | 20, 21 | oveq12d 7429 |
. . . . 5
β’ (πΉ β (π₯π»π¦) β ((domaβπΉ)π»(codaβπΉ)) = (π₯π»π¦)) |
23 | 19, 22 | eleqtrrd 2834 |
. . . 4
β’ (πΉ β (π₯π»π¦) β πΉ β ((domaβπΉ)π»(codaβπΉ))) |
24 | 23 | rexlimivw 3149 |
. . 3
β’
(βπ¦ β
(BaseβπΆ)πΉ β (π₯π»π¦) β πΉ β ((domaβπΉ)π»(codaβπΉ))) |
25 | 24 | rexlimivw 3149 |
. 2
β’
(βπ₯ β
(BaseβπΆ)βπ¦ β (BaseβπΆ)πΉ β (π₯π»π¦) β πΉ β ((domaβπΉ)π»(codaβπΉ))) |
26 | 18, 25 | syl 17 |
1
β’ (πΉ β π΄ β πΉ β ((domaβπΉ)π»(codaβπΉ))) |