Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ ((π β§ π½ β (SubcatβπΆ)) β π½ β (SubcatβπΆ)) |
2 | | issubc3.h |
. . . 4
β’ π» = (Homf
βπΆ) |
3 | 1, 2 | subcssc 17731 |
. . 3
β’ ((π β§ π½ β (SubcatβπΆ)) β π½ βcat π») |
4 | 1 | adantr 482 |
. . . . 5
β’ (((π β§ π½ β (SubcatβπΆ)) β§ π₯ β π) β π½ β (SubcatβπΆ)) |
5 | | issubc3.a |
. . . . . 6
β’ (π β π½ Fn (π Γ π)) |
6 | 5 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π½ β (SubcatβπΆ)) β§ π₯ β π) β π½ Fn (π Γ π)) |
7 | | simpr 486 |
. . . . 5
β’ (((π β§ π½ β (SubcatβπΆ)) β§ π₯ β π) β π₯ β π) |
8 | | issubc3.i |
. . . . 5
β’ 1 =
(IdβπΆ) |
9 | 4, 6, 7, 8 | subcidcl 17735 |
. . . 4
β’ (((π β§ π½ β (SubcatβπΆ)) β§ π₯ β π) β ( 1 βπ₯) β (π₯π½π₯)) |
10 | 9 | ralrimiva 3140 |
. . 3
β’ ((π β§ π½ β (SubcatβπΆ)) β βπ₯ β π ( 1 βπ₯) β (π₯π½π₯)) |
11 | | issubc3.1 |
. . . 4
β’ π· = (πΆ βΎcat π½) |
12 | 11, 1 | subccat 17739 |
. . 3
β’ ((π β§ π½ β (SubcatβπΆ)) β π· β Cat) |
13 | 3, 10, 12 | 3jca 1129 |
. 2
β’ ((π β§ π½ β (SubcatβπΆ)) β (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat)) |
14 | | simpr1 1195 |
. . 3
β’ ((π β§ (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat)) β π½ βcat π») |
15 | | simpr2 1196 |
. . . 4
β’ ((π β§ (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat)) β βπ₯ β π ( 1 βπ₯) β (π₯π½π₯)) |
16 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ·) =
(Baseβπ·) |
17 | | eqid 2733 |
. . . . . . . . . 10
β’ (Hom
βπ·) = (Hom
βπ·) |
18 | | eqid 2733 |
. . . . . . . . . 10
β’
(compβπ·) =
(compβπ·) |
19 | | simplrr 777 |
. . . . . . . . . 10
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π· β Cat) |
20 | | simprl1 1219 |
. . . . . . . . . . 11
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π₯ β π) |
21 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(BaseβπΆ) =
(BaseβπΆ) |
22 | | issubc3.c |
. . . . . . . . . . . . 13
β’ (π β πΆ β Cat) |
23 | 22 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β πΆ β Cat) |
24 | 5 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π½ Fn (π Γ π)) |
25 | 2, 21 | homffn 17578 |
. . . . . . . . . . . . . 14
β’ π» Fn ((BaseβπΆ) Γ (BaseβπΆ)) |
26 | 25 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π» Fn ((BaseβπΆ) Γ (BaseβπΆ))) |
27 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π½ βcat π») |
28 | 24, 26, 27 | ssc1 17709 |
. . . . . . . . . . . 12
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π β (BaseβπΆ)) |
29 | 11, 21, 23, 24, 28 | rescbas 17717 |
. . . . . . . . . . 11
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π = (Baseβπ·)) |
30 | 20, 29 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π₯ β (Baseβπ·)) |
31 | | simprl2 1220 |
. . . . . . . . . . 11
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π¦ β π) |
32 | 31, 29 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π¦ β (Baseβπ·)) |
33 | | simprl3 1221 |
. . . . . . . . . . 11
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π§ β π) |
34 | 33, 29 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π§ β (Baseβπ·)) |
35 | | simprrl 780 |
. . . . . . . . . . 11
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π β (π₯π½π¦)) |
36 | 11, 21, 23, 24, 28 | reschom 17719 |
. . . . . . . . . . . 12
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π½ = (Hom βπ·)) |
37 | 36 | oveqd 7375 |
. . . . . . . . . . 11
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β (π₯π½π¦) = (π₯(Hom βπ·)π¦)) |
38 | 35, 37 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π β (π₯(Hom βπ·)π¦)) |
39 | | simprrr 781 |
. . . . . . . . . . 11
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π β (π¦π½π§)) |
40 | 36 | oveqd 7375 |
. . . . . . . . . . 11
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β (π¦π½π§) = (π¦(Hom βπ·)π§)) |
41 | 39, 40 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β π β (π¦(Hom βπ·)π§)) |
42 | 16, 17, 18, 19, 30, 32, 34, 38, 41 | catcocl 17570 |
. . . . . . . . 9
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β (π(β¨π₯, π¦β©(compβπ·)π§)π) β (π₯(Hom βπ·)π§)) |
43 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(compβπΆ) =
(compβπΆ) |
44 | 11, 21, 23, 24, 28, 43 | rescco 17721 |
. . . . . . . . . . 11
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β (compβπΆ) = (compβπ·)) |
45 | 44 | oveqd 7375 |
. . . . . . . . . 10
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β (β¨π₯, π¦β©(compβπΆ)π§) = (β¨π₯, π¦β©(compβπ·)π§)) |
46 | 45 | oveqd 7375 |
. . . . . . . . 9
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) = (π(β¨π₯, π¦β©(compβπ·)π§)π)) |
47 | 36 | oveqd 7375 |
. . . . . . . . 9
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β (π₯π½π§) = (π₯(Hom βπ·)π§)) |
48 | 42, 46, 47 | 3eltr4d 2849 |
. . . . . . . 8
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§)))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π½π§)) |
49 | 48 | anassrs 469 |
. . . . . . 7
β’ ((((π β§ (π½ βcat π» β§ π· β Cat)) β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π β (π₯π½π¦) β§ π β (π¦π½π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π½π§)) |
50 | 49 | ralrimivva 3194 |
. . . . . 6
β’ (((π β§ (π½ βcat π» β§ π· β Cat)) β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π½π§)) |
51 | 50 | ralrimivvva 3197 |
. . . . 5
β’ ((π β§ (π½ βcat π» β§ π· β Cat)) β βπ₯ β π βπ¦ β π βπ§ β π βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π½π§)) |
52 | 51 | 3adantr2 1171 |
. . . 4
β’ ((π β§ (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat)) β βπ₯ β π βπ¦ β π βπ§ β π βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π½π§)) |
53 | | r19.26 3111 |
. . . 4
β’
(βπ₯ β
π (( 1 βπ₯) β (π₯π½π₯) β§ βπ¦ β π βπ§ β π βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π½π§)) β (βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π½π§))) |
54 | 15, 52, 53 | sylanbrc 584 |
. . 3
β’ ((π β§ (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat)) β βπ₯ β π (( 1 βπ₯) β (π₯π½π₯) β§ βπ¦ β π βπ§ β π βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π½π§))) |
55 | 22 | adantr 482 |
. . . 4
β’ ((π β§ (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat)) β πΆ β Cat) |
56 | 5 | adantr 482 |
. . . 4
β’ ((π β§ (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat)) β π½ Fn (π Γ π)) |
57 | 2, 8, 43, 55, 56 | issubc2 17727 |
. . 3
β’ ((π β§ (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat)) β (π½ β (SubcatβπΆ) β (π½ βcat π» β§ βπ₯ β π (( 1 βπ₯) β (π₯π½π₯) β§ βπ¦ β π βπ§ β π βπ β (π₯π½π¦)βπ β (π¦π½π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯π½π§))))) |
58 | 14, 54, 57 | mpbir2and 712 |
. 2
β’ ((π β§ (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat)) β π½ β (SubcatβπΆ)) |
59 | 13, 58 | impbida 800 |
1
β’ (π β (π½ β (SubcatβπΆ) β (π½ βcat π» β§ βπ₯ β π ( 1 βπ₯) β (π₯π½π₯) β§ π· β Cat))) |