Step | Hyp | Ref
| Expression |
1 | | setcbas.c |
. . . 4
β’ πΆ = (SetCatβπ) |
2 | | setcbas.u |
. . . 4
β’ (π β π β π) |
3 | | setcco.o |
. . . 4
β’ Β· =
(compβπΆ) |
4 | 1, 2, 3 | setccofval 17928 |
. . 3
β’ (π β Β· = (π£ β (π Γ π), π§ β π β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))) |
5 | | simprr 771 |
. . . . 5
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β π§ = π) |
6 | | simprl 769 |
. . . . . . 7
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β π£ = β¨π, πβ©) |
7 | 6 | fveq2d 6843 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (2nd βπ£) = (2nd
ββ¨π, πβ©)) |
8 | | setcco.x |
. . . . . . . 8
β’ (π β π β π) |
9 | | setcco.y |
. . . . . . . 8
β’ (π β π β π) |
10 | | op2ndg 7926 |
. . . . . . . 8
β’ ((π β π β§ π β π) β (2nd ββ¨π, πβ©) = π) |
11 | 8, 9, 10 | syl2anc 584 |
. . . . . . 7
β’ (π β (2nd
ββ¨π, πβ©) = π) |
12 | 11 | adantr 481 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (2nd ββ¨π, πβ©) = π) |
13 | 7, 12 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (2nd βπ£) = π) |
14 | 5, 13 | oveq12d 7369 |
. . . 4
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (π§ βm (2nd
βπ£)) = (π βm π)) |
15 | 6 | fveq2d 6843 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (1st βπ£) = (1st
ββ¨π, πβ©)) |
16 | | op1stg 7925 |
. . . . . . . 8
β’ ((π β π β§ π β π) β (1st ββ¨π, πβ©) = π) |
17 | 8, 9, 16 | syl2anc 584 |
. . . . . . 7
β’ (π β (1st
ββ¨π, πβ©) = π) |
18 | 17 | adantr 481 |
. . . . . 6
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (1st ββ¨π, πβ©) = π) |
19 | 15, 18 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (1st βπ£) = π) |
20 | 13, 19 | oveq12d 7369 |
. . . 4
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β ((2nd βπ£) βm
(1st βπ£))
= (π βm
π)) |
21 | | eqidd 2738 |
. . . 4
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (π β π) = (π β π)) |
22 | 14, 20, 21 | mpoeq123dv 7426 |
. . 3
β’ ((π β§ (π£ = β¨π, πβ© β§ π§ = π)) β (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)) = (π β (π βm π), π β (π βm π) β¦ (π β π))) |
23 | 8, 9 | opelxpd 5669 |
. . 3
β’ (π β β¨π, πβ© β (π Γ π)) |
24 | | setcco.z |
. . 3
β’ (π β π β π) |
25 | | ovex 7384 |
. . . . 5
β’ (π βm π) β V |
26 | | ovex 7384 |
. . . . 5
β’ (π βm π) β V |
27 | 25, 26 | mpoex 8004 |
. . . 4
β’ (π β (π βm π), π β (π βm π) β¦ (π β π)) β V |
28 | 27 | a1i 11 |
. . 3
β’ (π β (π β (π βm π), π β (π βm π) β¦ (π β π)) β V) |
29 | 4, 22, 23, 24, 28 | ovmpod 7501 |
. 2
β’ (π β (β¨π, πβ© Β· π) = (π β (π βm π), π β (π βm π) β¦ (π β π))) |
30 | | simprl 769 |
. . 3
β’ ((π β§ (π = πΊ β§ π = πΉ)) β π = πΊ) |
31 | | simprr 771 |
. . 3
β’ ((π β§ (π = πΊ β§ π = πΉ)) β π = πΉ) |
32 | 30, 31 | coeq12d 5818 |
. 2
β’ ((π β§ (π = πΊ β§ π = πΉ)) β (π β π) = (πΊ β πΉ)) |
33 | | setcco.g |
. . 3
β’ (π β πΊ:πβΆπ) |
34 | 24, 9 | elmapd 8737 |
. . 3
β’ (π β (πΊ β (π βm π) β πΊ:πβΆπ)) |
35 | 33, 34 | mpbird 256 |
. 2
β’ (π β πΊ β (π βm π)) |
36 | | setcco.f |
. . 3
β’ (π β πΉ:πβΆπ) |
37 | 9, 8 | elmapd 8737 |
. . 3
β’ (π β (πΉ β (π βm π) β πΉ:πβΆπ)) |
38 | 36, 37 | mpbird 256 |
. 2
β’ (π β πΉ β (π βm π)) |
39 | | coexg 7858 |
. . 3
β’ ((πΊ β (π βm π) β§ πΉ β (π βm π)) β (πΊ β πΉ) β V) |
40 | 35, 38, 39 | syl2anc 584 |
. 2
β’ (π β (πΊ β πΉ) β V) |
41 | 29, 32, 35, 38, 40 | ovmpod 7501 |
1
β’ (π β (πΊ(β¨π, πβ© Β· π)πΉ) = (πΊ β πΉ)) |