Step | Hyp | Ref
| Expression |
1 | | df-br 5111 |
. 2
β’ (πΊdom Β· πΉ β β¨πΊ, πΉβ© β dom Β· ) |
2 | | otex 5427 |
. . . . . 6
β’
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β©(compβπΆ)(codaβπ))(2nd βπ))β© β
V |
3 | 2 | rgen2w 3070 |
. . . . 5
β’
βπ β
π΄ βπ β {β β π΄ β£ (codaββ) =
(domaβπ)}β¨(domaβπ),
(codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β©(compβπΆ)(codaβπ))(2nd βπ))β© β
V |
4 | | coafval.o |
. . . . . . 7
β’ Β· =
(compaβπΆ) |
5 | | coafval.a |
. . . . . . 7
β’ π΄ = (ArrowβπΆ) |
6 | | eqid 2737 |
. . . . . . 7
β’
(compβπΆ) =
(compβπΆ) |
7 | 4, 5, 6 | coafval 17957 |
. . . . . 6
β’ Β· =
(π β π΄, π β {β β π΄ β£ (codaββ) =
(domaβπ)} β¦
β¨(domaβπ), (codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β©(compβπΆ)(codaβπ))(2nd βπ))β©) |
8 | 7 | fmpox 8004 |
. . . . 5
β’
(βπ β
π΄ βπ β {β β π΄ β£ (codaββ) =
(domaβπ)}β¨(domaβπ),
(codaβπ), ((2nd βπ)(β¨(domaβπ),
(domaβπ)β©(compβπΆ)(codaβπ))(2nd βπ))β© β V β Β·
:βͺ π β π΄ ({π} Γ {β β π΄ β£ (codaββ) =
(domaβπ)})βΆV) |
9 | 3, 8 | mpbi 229 |
. . . 4
β’ Β·
:βͺ π β π΄ ({π} Γ {β β π΄ β£ (codaββ) =
(domaβπ)})βΆV |
10 | 9 | fdmi 6685 |
. . 3
β’ dom Β· =
βͺ π β π΄ ({π} Γ {β β π΄ β£ (codaββ) =
(domaβπ)}) |
11 | 10 | eleq2i 2830 |
. 2
β’
(β¨πΊ, πΉβ© β dom Β· β
β¨πΊ, πΉβ© β βͺ π β π΄ ({π} Γ {β β π΄ β£ (codaββ) =
(domaβπ)})) |
12 | | fveq2 6847 |
. . . . . 6
β’ (π = πΊ β (domaβπ) =
(domaβπΊ)) |
13 | 12 | eqeq2d 2748 |
. . . . 5
β’ (π = πΊ β ((codaββ) =
(domaβπ) β (codaββ) =
(domaβπΊ))) |
14 | 13 | rabbidv 3418 |
. . . 4
β’ (π = πΊ β {β β π΄ β£ (codaββ) =
(domaβπ)} = {β β π΄ β£ (codaββ) =
(domaβπΊ)}) |
15 | 14 | opeliunxp2 5799 |
. . 3
β’
(β¨πΊ, πΉβ© β βͺ π β π΄ ({π} Γ {β β π΄ β£ (codaββ) =
(domaβπ)}) β (πΊ β π΄ β§ πΉ β {β β π΄ β£ (codaββ) =
(domaβπΊ)})) |
16 | | fveqeq2 6856 |
. . . . 5
β’ (β = πΉ β ((codaββ) =
(domaβπΊ) β (codaβπΉ) =
(domaβπΊ))) |
17 | 16 | elrab 3650 |
. . . 4
β’ (πΉ β {β β π΄ β£ (codaββ) =
(domaβπΊ)} β (πΉ β π΄ β§ (codaβπΉ) =
(domaβπΊ))) |
18 | 17 | anbi2i 624 |
. . 3
β’ ((πΊ β π΄ β§ πΉ β {β β π΄ β£ (codaββ) =
(domaβπΊ)}) β (πΊ β π΄ β§ (πΉ β π΄ β§ (codaβπΉ) =
(domaβπΊ)))) |
19 | | an12 644 |
. . . 4
β’ ((πΊ β π΄ β§ (πΉ β π΄ β§ (codaβπΉ) =
(domaβπΊ))) β (πΉ β π΄ β§ (πΊ β π΄ β§ (codaβπΉ) =
(domaβπΊ)))) |
20 | | 3anass 1096 |
. . . 4
β’ ((πΉ β π΄ β§ πΊ β π΄ β§ (codaβπΉ) =
(domaβπΊ)) β (πΉ β π΄ β§ (πΊ β π΄ β§ (codaβπΉ) =
(domaβπΊ)))) |
21 | 19, 20 | bitr4i 278 |
. . 3
β’ ((πΊ β π΄ β§ (πΉ β π΄ β§ (codaβπΉ) =
(domaβπΊ))) β (πΉ β π΄ β§ πΊ β π΄ β§ (codaβπΉ) =
(domaβπΊ))) |
22 | 15, 18, 21 | 3bitri 297 |
. 2
β’
(β¨πΊ, πΉβ© β βͺ π β π΄ ({π} Γ {β β π΄ β£ (codaββ) =
(domaβπ)}) β (πΉ β π΄ β§ πΊ β π΄ β§ (codaβπΉ) =
(domaβπΊ))) |
23 | 1, 11, 22 | 3bitri 297 |
1
β’ (πΊdom Β· πΉ β (πΉ β π΄ β§ πΊ β π΄ β§ (codaβπΉ) =
(domaβπΊ))) |