Step | Hyp | Ref
| Expression |
1 | | fullsubc.h |
. . . . 5
β’ π» = (Homf
βπΆ) |
2 | | fullsubc.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
3 | 1, 2 | homffn 17581 |
. . . 4
β’ π» Fn (π΅ Γ π΅) |
4 | 2 | fvexi 6860 |
. . . 4
β’ π΅ β V |
5 | | sscres 17714 |
. . . 4
β’ ((π» Fn (π΅ Γ π΅) β§ π΅ β V) β (π» βΎ (π Γ π)) βcat π») |
6 | 3, 4, 5 | mp2an 691 |
. . 3
β’ (π» βΎ (π Γ π)) βcat π» |
7 | 6 | a1i 11 |
. 2
β’ (π β (π» βΎ (π Γ π)) βcat π») |
8 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπΆ) = (Hom
βπΆ) |
9 | | eqid 2733 |
. . . . . 6
β’
(IdβπΆ) =
(IdβπΆ) |
10 | | fullsubc.c |
. . . . . . 7
β’ (π β πΆ β Cat) |
11 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π) β πΆ β Cat) |
12 | | fullsubc.s |
. . . . . . 7
β’ (π β π β π΅) |
13 | 12 | sselda 3948 |
. . . . . 6
β’ ((π β§ π₯ β π) β π₯ β π΅) |
14 | 2, 8, 9, 11, 13 | catidcl 17570 |
. . . . 5
β’ ((π β§ π₯ β π) β ((IdβπΆ)βπ₯) β (π₯(Hom βπΆ)π₯)) |
15 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π₯ β π) |
16 | 15, 15 | ovresd 7525 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π₯(π» βΎ (π Γ π))π₯) = (π₯π»π₯)) |
17 | 1, 2, 8, 13, 13 | homfval 17580 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π₯π»π₯) = (π₯(Hom βπΆ)π₯)) |
18 | 16, 17 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π₯ β π) β (π₯(π» βΎ (π Γ π))π₯) = (π₯(Hom βπΆ)π₯)) |
19 | 14, 18 | eleqtrrd 2837 |
. . . 4
β’ ((π β§ π₯ β π) β ((IdβπΆ)βπ₯) β (π₯(π» βΎ (π Γ π))π₯)) |
20 | | eqid 2733 |
. . . . . . . . . 10
β’
(compβπΆ) =
(compβπΆ) |
21 | 11 | ad3antrrr 729 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β πΆ β Cat) |
22 | 13 | ad3antrrr 729 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β π₯ β π΅) |
23 | 12 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β π β π΅) |
24 | 23 | sselda 3948 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π¦ β π) β π¦ β π΅) |
25 | 24 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π¦ β π΅) |
26 | 25 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β π¦ β π΅) |
27 | 23 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π¦ β π) β π β π΅) |
28 | 27 | sselda 3948 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π§ β π΅) |
29 | 28 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β π§ β π΅) |
30 | | simprl 770 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β π β (π₯(Hom βπΆ)π¦)) |
31 | | simprr 772 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β π β (π¦(Hom βπΆ)π§)) |
32 | 2, 8, 20, 21, 22, 26, 29, 30, 31 | catcocl 17573 |
. . . . . . . . 9
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(Hom βπΆ)π§)) |
33 | 15 | ad3antrrr 729 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β π₯ β π) |
34 | | simplr 768 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β π§ β π) |
35 | 33, 34 | ovresd 7525 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β (π₯(π» βΎ (π Γ π))π§) = (π₯π»π§)) |
36 | 1, 2, 8, 22, 29 | homfval 17580 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β (π₯π»π§) = (π₯(Hom βπΆ)π§)) |
37 | 35, 36 | eqtrd 2773 |
. . . . . . . . 9
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β (π₯(π» βΎ (π Γ π))π§) = (π₯(Hom βπΆ)π§)) |
38 | 32, 37 | eleqtrrd 2837 |
. . . . . . . 8
β’
(((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β§ (π β (π₯(Hom βπΆ)π¦) β§ π β (π¦(Hom βπΆ)π§))) β (π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§)) |
39 | 38 | ralrimivva 3194 |
. . . . . . 7
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β βπ β (π₯(Hom βπΆ)π¦)βπ β (π¦(Hom βπΆ)π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§)) |
40 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π¦ β π) β π₯ β π) |
41 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π¦ β π) β π¦ β π) |
42 | 40, 41 | ovresd 7525 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π¦ β π) β (π₯(π» βΎ (π Γ π))π¦) = (π₯π»π¦)) |
43 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π¦ β π) β π₯ β π΅) |
44 | 1, 2, 8, 43, 24 | homfval 17580 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π¦ β π) β (π₯π»π¦) = (π₯(Hom βπΆ)π¦)) |
45 | 42, 44 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π¦ β π) β (π₯(π» βΎ (π Γ π))π¦) = (π₯(Hom βπΆ)π¦)) |
46 | 45 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (π₯(π» βΎ (π Γ π))π¦) = (π₯(Hom βπΆ)π¦)) |
47 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π¦ β π) |
48 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β π§ β π) |
49 | 47, 48 | ovresd 7525 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (π¦(π» βΎ (π Γ π))π§) = (π¦π»π§)) |
50 | 1, 2, 8, 25, 28 | homfval 17580 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (π¦π»π§) = (π¦(Hom βπΆ)π§)) |
51 | 49, 50 | eqtrd 2773 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (π¦(π» βΎ (π Γ π))π§) = (π¦(Hom βπΆ)π§)) |
52 | 51 | raleqdv 3312 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (βπ β (π¦(π» βΎ (π Γ π))π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§) β βπ β (π¦(Hom βπΆ)π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§))) |
53 | 46, 52 | raleqbidv 3318 |
. . . . . . 7
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β (βπ β (π₯(π» βΎ (π Γ π))π¦)βπ β (π¦(π» βΎ (π Γ π))π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§) β βπ β (π₯(Hom βπΆ)π¦)βπ β (π¦(Hom βπΆ)π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§))) |
54 | 39, 53 | mpbird 257 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ π§ β π) β βπ β (π₯(π» βΎ (π Γ π))π¦)βπ β (π¦(π» βΎ (π Γ π))π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§)) |
55 | 54 | ralrimiva 3140 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β βπ§ β π βπ β (π₯(π» βΎ (π Γ π))π¦)βπ β (π¦(π» βΎ (π Γ π))π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§)) |
56 | 55 | ralrimiva 3140 |
. . . 4
β’ ((π β§ π₯ β π) β βπ¦ β π βπ§ β π βπ β (π₯(π» βΎ (π Γ π))π¦)βπ β (π¦(π» βΎ (π Γ π))π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§)) |
57 | 19, 56 | jca 513 |
. . 3
β’ ((π β§ π₯ β π) β (((IdβπΆ)βπ₯) β (π₯(π» βΎ (π Γ π))π₯) β§ βπ¦ β π βπ§ β π βπ β (π₯(π» βΎ (π Γ π))π¦)βπ β (π¦(π» βΎ (π Γ π))π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§))) |
58 | 57 | ralrimiva 3140 |
. 2
β’ (π β βπ₯ β π (((IdβπΆ)βπ₯) β (π₯(π» βΎ (π Γ π))π₯) β§ βπ¦ β π βπ§ β π βπ β (π₯(π» βΎ (π Γ π))π¦)βπ β (π¦(π» βΎ (π Γ π))π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§))) |
59 | | xpss12 5652 |
. . . . 5
β’ ((π β π΅ β§ π β π΅) β (π Γ π) β (π΅ Γ π΅)) |
60 | 12, 12, 59 | syl2anc 585 |
. . . 4
β’ (π β (π Γ π) β (π΅ Γ π΅)) |
61 | | fnssres 6628 |
. . . 4
β’ ((π» Fn (π΅ Γ π΅) β§ (π Γ π) β (π΅ Γ π΅)) β (π» βΎ (π Γ π)) Fn (π Γ π)) |
62 | 3, 60, 61 | sylancr 588 |
. . 3
β’ (π β (π» βΎ (π Γ π)) Fn (π Γ π)) |
63 | 1, 9, 20, 10, 62 | issubc2 17730 |
. 2
β’ (π β ((π» βΎ (π Γ π)) β (SubcatβπΆ) β ((π» βΎ (π Γ π)) βcat π» β§ βπ₯ β π (((IdβπΆ)βπ₯) β (π₯(π» βΎ (π Γ π))π₯) β§ βπ¦ β π βπ§ β π βπ β (π₯(π» βΎ (π Γ π))π¦)βπ β (π¦(π» βΎ (π Γ π))π§)(π(β¨π₯, π¦β©(compβπΆ)π§)π) β (π₯(π» βΎ (π Γ π))π§))))) |
64 | 7, 58, 63 | mpbir2and 712 |
1
β’ (π β (π» βΎ (π Γ π)) β (SubcatβπΆ)) |