Step | Hyp | Ref
| Expression |
1 | | setcval.c |
. 2
β’ πΆ = (SetCatβπ) |
2 | | df-setc 17922 |
. . 3
β’ SetCat =
(π’ β V β¦
{β¨(Baseβndx), π’β©, β¨(Hom βndx), (π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯))β©, β¨(compβndx), (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))β©}) |
3 | | simpr 485 |
. . . . 5
β’ ((π β§ π’ = π) β π’ = π) |
4 | 3 | opeq2d 4835 |
. . . 4
β’ ((π β§ π’ = π) β β¨(Baseβndx), π’β© = β¨(Baseβndx),
πβ©) |
5 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ π’ = π) β (π¦ βm π₯) = (π¦ βm π₯)) |
6 | 3, 3, 5 | mpoeq123dv 7426 |
. . . . . 6
β’ ((π β§ π’ = π) β (π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯)) = (π₯ β π, π¦ β π β¦ (π¦ βm π₯))) |
7 | | setcval.h |
. . . . . . 7
β’ (π β π» = (π₯ β π, π¦ β π β¦ (π¦ βm π₯))) |
8 | 7 | adantr 481 |
. . . . . 6
β’ ((π β§ π’ = π) β π» = (π₯ β π, π¦ β π β¦ (π¦ βm π₯))) |
9 | 6, 8 | eqtr4d 2780 |
. . . . 5
β’ ((π β§ π’ = π) β (π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯)) = π») |
10 | 9 | opeq2d 4835 |
. . . 4
β’ ((π β§ π’ = π) β β¨(Hom βndx), (π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯))β© = β¨(Hom βndx), π»β©) |
11 | 3 | sqxpeqd 5663 |
. . . . . . 7
β’ ((π β§ π’ = π) β (π’ Γ π’) = (π Γ π)) |
12 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ π’ = π) β (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)) = (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π))) |
13 | 11, 3, 12 | mpoeq123dv 7426 |
. . . . . 6
β’ ((π β§ π’ = π) β (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π))) = (π£ β (π Γ π), π§ β π β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))) |
14 | | setcval.o |
. . . . . . 7
β’ (π β Β· = (π£ β (π Γ π), π§ β π β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))) |
15 | 14 | adantr 481 |
. . . . . 6
β’ ((π β§ π’ = π) β Β· = (π£ β (π Γ π), π§ β π β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))) |
16 | 13, 15 | eqtr4d 2780 |
. . . . 5
β’ ((π β§ π’ = π) β (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π))) = Β· ) |
17 | 16 | opeq2d 4835 |
. . . 4
β’ ((π β§ π’ = π) β β¨(compβndx), (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))β© = β¨(compβndx), Β·
β©) |
18 | 4, 10, 17 | tpeq123d 4707 |
. . 3
β’ ((π β§ π’ = π) β {β¨(Baseβndx), π’β©, β¨(Hom βndx),
(π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯))β©, β¨(compβndx), (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))β©} = {β¨(Baseβndx), πβ©, β¨(Hom βndx),
π»β©,
β¨(compβndx), Β·
β©}) |
19 | | setcval.u |
. . . 4
β’ (π β π β π) |
20 | 19 | elexd 3463 |
. . 3
β’ (π β π β V) |
21 | | tpex 7673 |
. . . 4
β’
{β¨(Baseβndx), πβ©, β¨(Hom βndx), π»β©, β¨(compβndx),
Β·
β©} β V |
22 | 21 | a1i 11 |
. . 3
β’ (π β {β¨(Baseβndx),
πβ©, β¨(Hom
βndx), π»β©,
β¨(compβndx), Β· β©} β
V) |
23 | 2, 18, 20, 22 | fvmptd2 6953 |
. 2
β’ (π β (SetCatβπ) = {β¨(Baseβndx),
πβ©, β¨(Hom
βndx), π»β©,
β¨(compβndx), Β·
β©}) |
24 | 1, 23 | eqtrid 2789 |
1
β’ (π β πΆ = {β¨(Baseβndx), πβ©, β¨(Hom βndx),
π»β©,
β¨(compβndx), Β·
β©}) |