Step | Hyp | Ref
| Expression |
1 | | oppcco.x |
. . . . 5
β’ (π β π β π΅) |
2 | | elfvex 6884 |
. . . . . 6
β’ (π β (BaseβπΆ) β πΆ β V) |
3 | | oppcco.b |
. . . . . 6
β’ π΅ = (BaseβπΆ) |
4 | 2, 3 | eleq2s 2852 |
. . . . 5
β’ (π β π΅ β πΆ β V) |
5 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπΆ) = (Hom
βπΆ) |
6 | | oppcco.c |
. . . . . 6
β’ Β· =
(compβπΆ) |
7 | | oppcco.o |
. . . . . 6
β’ π = (oppCatβπΆ) |
8 | 3, 5, 6, 7 | oppcval 17601 |
. . . . 5
β’ (πΆ β V β π = ((πΆ sSet β¨(Hom βndx), tpos (Hom
βπΆ)β©) sSet
β¨(compβndx), (π’
β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©)) |
9 | 1, 4, 8 | 3syl 18 |
. . . 4
β’ (π β π = ((πΆ sSet β¨(Hom βndx), tpos (Hom
βπΆ)β©) sSet
β¨(compβndx), (π’
β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©)) |
10 | 9 | fveq2d 6850 |
. . 3
β’ (π β (compβπ) = (compβ((πΆ sSet β¨(Hom βndx),
tpos (Hom βπΆ)β©)
sSet β¨(compβndx), (π’ β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©))) |
11 | | ovex 7394 |
. . . 4
β’ (πΆ sSet β¨(Hom βndx),
tpos (Hom βπΆ)β©)
β V |
12 | 3 | fvexi 6860 |
. . . . . 6
β’ π΅ β V |
13 | 12, 12 | xpex 7691 |
. . . . 5
β’ (π΅ Γ π΅) β V |
14 | 13, 12 | mpoex 8016 |
. . . 4
β’ (π’ β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’))) β
V |
15 | | ccoid 17303 |
. . . . 5
β’ comp =
Slot (compβndx) |
16 | 15 | setsid 17088 |
. . . 4
β’ (((πΆ sSet β¨(Hom βndx),
tpos (Hom βπΆ)β©)
β V β§ (π’ β
(π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’))) β V)
β (π’ β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’))) =
(compβ((πΆ sSet
β¨(Hom βndx), tpos (Hom βπΆ)β©) sSet β¨(compβndx), (π’ β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©))) |
17 | 11, 14, 16 | mp2an 691 |
. . 3
β’ (π’ β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’))) =
(compβ((πΆ sSet
β¨(Hom βndx), tpos (Hom βπΆ)β©) sSet β¨(compβndx), (π’ β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))β©)) |
18 | 10, 17 | eqtr4di 2791 |
. 2
β’ (π β (compβπ) = (π’ β (π΅ Γ π΅), π§ β π΅ β¦ tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)))) |
19 | | simprr 772 |
. . . . 5
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β π§ = π) |
20 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β π’ = β¨π, πβ©) |
21 | 20 | fveq2d 6850 |
. . . . . 6
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β (2nd βπ’) = (2nd
ββ¨π, πβ©)) |
22 | | oppcco.y |
. . . . . . . 8
β’ (π β π β π΅) |
23 | 22 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β π β π΅) |
24 | | op2ndg 7938 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β (2nd ββ¨π, πβ©) = π) |
25 | 1, 23, 24 | syl2an2r 684 |
. . . . . 6
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β (2nd ββ¨π, πβ©) = π) |
26 | 21, 25 | eqtrd 2773 |
. . . . 5
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β (2nd βπ’) = π) |
27 | 19, 26 | opeq12d 4842 |
. . . 4
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β β¨π§, (2nd βπ’)β© = β¨π, πβ©) |
28 | 20 | fveq2d 6850 |
. . . . 5
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β (1st βπ’) = (1st
ββ¨π, πβ©)) |
29 | | op1stg 7937 |
. . . . . 6
β’ ((π β π΅ β§ π β π΅) β (1st ββ¨π, πβ©) = π) |
30 | 1, 23, 29 | syl2an2r 684 |
. . . . 5
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β (1st ββ¨π, πβ©) = π) |
31 | 28, 30 | eqtrd 2773 |
. . . 4
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β (1st βπ’) = π) |
32 | 27, 31 | oveq12d 7379 |
. . 3
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)) = (β¨π, πβ© Β· π)) |
33 | 32 | tposeqd 8164 |
. 2
β’ ((π β§ (π’ = β¨π, πβ© β§ π§ = π)) β tpos (β¨π§, (2nd βπ’)β© Β· (1st
βπ’)) = tpos
(β¨π, πβ© Β· π)) |
34 | 1, 22 | opelxpd 5675 |
. 2
β’ (π β β¨π, πβ© β (π΅ Γ π΅)) |
35 | | oppcco.z |
. 2
β’ (π β π β π΅) |
36 | | ovex 7394 |
. . . 4
β’
(β¨π, πβ© Β· π) β V |
37 | 36 | tposex 8195 |
. . 3
β’ tpos
(β¨π, πβ© Β· π) β V |
38 | 37 | a1i 11 |
. 2
β’ (π β tpos (β¨π, πβ© Β· π) β V) |
39 | 18, 33, 34, 35, 38 | ovmpod 7511 |
1
β’ (π β (β¨π, πβ©(compβπ)π) = tpos (β¨π, πβ© Β· π)) |