Step | Hyp | Ref
| Expression |
1 | | oppcval.o |
. 2
β’ π = (oppCatβπΆ) |
2 | | elex 3461 |
. . 3
β’ (πΆ β π β πΆ β V) |
3 | | id 22 |
. . . . . 6
β’ (π = πΆ β π = πΆ) |
4 | | fveq2 6839 |
. . . . . . . . 9
β’ (π = πΆ β (Hom βπ) = (Hom βπΆ)) |
5 | | oppcval.h |
. . . . . . . . 9
β’ π» = (Hom βπΆ) |
6 | 4, 5 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = πΆ β (Hom βπ) = π») |
7 | 6 | tposeqd 8152 |
. . . . . . 7
β’ (π = πΆ β tpos (Hom βπ) = tpos π») |
8 | 7 | opeq2d 4835 |
. . . . . 6
β’ (π = πΆ β β¨(Hom βndx), tpos (Hom
βπ)β© =
β¨(Hom βndx), tpos π»β©) |
9 | 3, 8 | oveq12d 7369 |
. . . . 5
β’ (π = πΆ β (π sSet β¨(Hom βndx), tpos (Hom
βπ)β©) = (πΆ sSet β¨(Hom βndx),
tpos π»β©)) |
10 | | fveq2 6839 |
. . . . . . . . 9
β’ (π = πΆ β (Baseβπ) = (BaseβπΆ)) |
11 | | oppcval.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΆ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = πΆ β (Baseβπ) = π΅) |
13 | 12 | sqxpeqd 5663 |
. . . . . . 7
β’ (π = πΆ β ((Baseβπ) Γ (Baseβπ)) = (π΅ Γ π΅)) |
14 | | fveq2 6839 |
. . . . . . . . . 10
β’ (π = πΆ β (compβπ) = (compβπΆ)) |
15 | | oppcval.x |
. . . . . . . . . 10
β’ Β· =
(compβπΆ) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π = πΆ β (compβπ) = Β· ) |
17 | 16 | oveqd 7368 |
. . . . . . . 8
β’ (π = πΆ β (β¨π§, (2nd βπ’)β©(compβπ)(1st βπ’)) = (β¨π§, (2nd βπ’)β© Β· (1st
βπ’))) |
18 | 17 | tposeqd 8152 |
. . . . . . 7
β’ (π = πΆ β tpos (β¨π§, (2nd βπ’)β©(compβπ)(1st βπ’)) = tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’))) |
19 | 13, 12, 18 | mpoeq123dv 7426 |
. . . . . 6
β’ (π = πΆ β (π’ β ((Baseβπ) Γ (Baseβπ)), π§ β (Baseβπ) β¦ tpos (β¨π§, (2nd βπ’)β©(compβπ)(1st βπ’))) = (π’ β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))) |
20 | 19 | opeq2d 4835 |
. . . . 5
β’ (π = πΆ β β¨(compβndx), (π’ β ((Baseβπ) Γ (Baseβπ)), π§ β (Baseβπ) β¦ tpos (β¨π§, (2nd βπ’)β©(compβπ)(1st βπ’)))β© = β¨(compβndx), (π’ β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©) |
21 | 9, 20 | oveq12d 7369 |
. . . 4
β’ (π = πΆ β ((π sSet β¨(Hom βndx), tpos (Hom
βπ)β©) sSet
β¨(compβndx), (π’
β ((Baseβπ)
Γ (Baseβπ)),
π§ β (Baseβπ) β¦ tpos (β¨π§, (2nd βπ’)β©(compβπ)(1st βπ’)))β©) = ((πΆ sSet β¨(Hom βndx), tpos π»β©) sSet
β¨(compβndx), (π’
β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©)) |
22 | | df-oppc 17552 |
. . . 4
β’ oppCat =
(π β V β¦ ((π sSet β¨(Hom βndx),
tpos (Hom βπ)β©)
sSet β¨(compβndx), (π’ β ((Baseβπ) Γ (Baseβπ)), π§ β (Baseβπ) β¦ tpos (β¨π§, (2nd βπ’)β©(compβπ)(1st βπ’)))β©)) |
23 | | ovex 7384 |
. . . 4
β’ ((πΆ sSet β¨(Hom βndx),
tpos π»β©) sSet
β¨(compβndx), (π’
β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©) β
V |
24 | 21, 22, 23 | fvmpt 6945 |
. . 3
β’ (πΆ β V β
(oppCatβπΆ) = ((πΆ sSet β¨(Hom βndx),
tpos π»β©) sSet
β¨(compβndx), (π’
β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©)) |
25 | 2, 24 | syl 17 |
. 2
β’ (πΆ β π β (oppCatβπΆ) = ((πΆ sSet β¨(Hom βndx), tpos π»β©) sSet
β¨(compβndx), (π’
β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©)) |
26 | 1, 25 | eqtrid 2789 |
1
β’ (πΆ β π β π = ((πΆ sSet β¨(Hom βndx), tpos π»β©) sSet
β¨(compβndx), (π’
β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©)) |