Step | Hyp | Ref
| Expression |
1 | | relfunc 17756 |
. . . 4
β’ Rel
(πΆ Func π) |
2 | | yoniso.y |
. . . . 5
β’ π = (YonβπΆ) |
3 | | yoniso.d |
. . . . . . . 8
β’ π· = (CatCatβπ) |
4 | | yoniso.b |
. . . . . . . 8
β’ π΅ = (Baseβπ·) |
5 | | yoniso.v |
. . . . . . . 8
β’ (π β π β π) |
6 | 3, 4, 5 | catcbas 17995 |
. . . . . . 7
β’ (π β π΅ = (π β© Cat)) |
7 | | inss2 4193 |
. . . . . . 7
β’ (π β© Cat) β
Cat |
8 | 6, 7 | eqsstrdi 4002 |
. . . . . 6
β’ (π β π΅ β Cat) |
9 | | yoniso.c |
. . . . . 6
β’ (π β πΆ β π΅) |
10 | 8, 9 | sseldd 3949 |
. . . . 5
β’ (π β πΆ β Cat) |
11 | | yoniso.o |
. . . . 5
β’ π = (oppCatβπΆ) |
12 | | yoniso.s |
. . . . 5
β’ π = (SetCatβπ) |
13 | | yoniso.q |
. . . . 5
β’ π = (π FuncCat π) |
14 | | yoniso.u |
. . . . 5
β’ (π β π β π) |
15 | | yoniso.h |
. . . . 5
β’ (π β ran
(Homf βπΆ) β π) |
16 | 2, 10, 11, 12, 13, 14, 15 | yoncl 18159 |
. . . 4
β’ (π β π β (πΆ Func π)) |
17 | | 1st2nd 7975 |
. . . 4
β’ ((Rel
(πΆ Func π) β§ π β (πΆ Func π)) β π = β¨(1st βπ), (2nd βπ)β©) |
18 | 1, 16, 17 | sylancr 588 |
. . 3
β’ (π β π = β¨(1st βπ), (2nd βπ)β©) |
19 | 2, 11, 12, 13, 10, 14, 15 | yonffth 18181 |
. . . . 5
β’ (π β π β ((πΆ Full π) β© (πΆ Faith π))) |
20 | 18, 19 | eqeltrrd 2835 |
. . . 4
β’ (π β β¨(1st
βπ), (2nd
βπ)β© β
((πΆ Full π) β© (πΆ Faith π))) |
21 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΆ) =
(BaseβπΆ) |
22 | | yoniso.e |
. . . . . 6
β’ πΈ = (π βΎs ran (1st
βπ)) |
23 | 11 | oppccat 17612 |
. . . . . . . 8
β’ (πΆ β Cat β π β Cat) |
24 | 10, 23 | syl 17 |
. . . . . . 7
β’ (π β π β Cat) |
25 | 12 | setccat 17979 |
. . . . . . . 8
β’ (π β π β π β Cat) |
26 | 14, 25 | syl 17 |
. . . . . . 7
β’ (π β π β Cat) |
27 | 13, 24, 26 | fuccat 17867 |
. . . . . 6
β’ (π β π β Cat) |
28 | | fvex 6859 |
. . . . . . . 8
β’
(1st βπ) β V |
29 | 28 | rnex 7853 |
. . . . . . 7
β’ ran
(1st βπ)
β V |
30 | 29 | a1i 11 |
. . . . . 6
β’ (π β ran (1st
βπ) β
V) |
31 | 13 | fucbas 17856 |
. . . . . . . . 9
β’ (π Func π) = (Baseβπ) |
32 | | 1st2ndbr 7978 |
. . . . . . . . . 10
β’ ((Rel
(πΆ Func π) β§ π β (πΆ Func π)) β (1st βπ)(πΆ Func π)(2nd βπ)) |
33 | 1, 16, 32 | sylancr 588 |
. . . . . . . . 9
β’ (π β (1st
βπ)(πΆ Func π)(2nd βπ)) |
34 | 21, 31, 33 | funcf1 17760 |
. . . . . . . 8
β’ (π β (1st
βπ):(BaseβπΆ)βΆ(π Func π)) |
35 | 34 | ffnd 6673 |
. . . . . . 7
β’ (π β (1st
βπ) Fn
(BaseβπΆ)) |
36 | | dffn3 6685 |
. . . . . . 7
β’
((1st βπ) Fn (BaseβπΆ) β (1st βπ):(BaseβπΆ)βΆran (1st βπ)) |
37 | 35, 36 | sylib 217 |
. . . . . 6
β’ (π β (1st
βπ):(BaseβπΆ)βΆran (1st
βπ)) |
38 | 21, 22, 27, 30, 37 | ffthres2c 17835 |
. . . . 5
β’ (π β ((1st
βπ)((πΆ Full π) β© (πΆ Faith π))(2nd βπ) β (1st βπ)((πΆ Full πΈ) β© (πΆ Faith πΈ))(2nd βπ))) |
39 | | df-br 5110 |
. . . . 5
β’
((1st βπ)((πΆ Full π) β© (πΆ Faith π))(2nd βπ) β β¨(1st βπ), (2nd βπ)β© β ((πΆ Full π) β© (πΆ Faith π))) |
40 | | df-br 5110 |
. . . . 5
β’
((1st βπ)((πΆ Full πΈ) β© (πΆ Faith πΈ))(2nd βπ) β β¨(1st βπ), (2nd βπ)β© β ((πΆ Full πΈ) β© (πΆ Faith πΈ))) |
41 | 38, 39, 40 | 3bitr3g 313 |
. . . 4
β’ (π β (β¨(1st
βπ), (2nd
βπ)β© β
((πΆ Full π) β© (πΆ Faith π)) β β¨(1st βπ), (2nd βπ)β© β ((πΆ Full πΈ) β© (πΆ Faith πΈ)))) |
42 | 20, 41 | mpbid 231 |
. . 3
β’ (π β β¨(1st
βπ), (2nd
βπ)β© β
((πΆ Full πΈ) β© (πΆ Faith πΈ))) |
43 | 18, 42 | eqeltrd 2834 |
. 2
β’ (π β π β ((πΆ Full πΈ) β© (πΆ Faith πΈ))) |
44 | | fveq2 6846 |
. . . . . . . . 9
β’
(((1st βπ)βπ₯) = ((1st βπ)βπ¦) β (1st
β((1st βπ)βπ₯)) = (1st β((1st
βπ)βπ¦))) |
45 | 44 | fveq1d 6848 |
. . . . . . . 8
β’
(((1st βπ)βπ₯) = ((1st βπ)βπ¦) β ((1st
β((1st βπ)βπ₯))βπ₯) = ((1st β((1st
βπ)βπ¦))βπ₯)) |
46 | 45 | fveq2d 6850 |
. . . . . . 7
β’
(((1st βπ)βπ₯) = ((1st βπ)βπ¦) β (πΉβ((1st
β((1st βπ)βπ₯))βπ₯)) = (πΉβ((1st
β((1st βπ)βπ¦))βπ₯))) |
47 | | simpl 484 |
. . . . . . . . . 10
β’ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β π₯ β (BaseβπΆ)) |
48 | 47, 47 | jca 513 |
. . . . . . . . 9
β’ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β (π₯ β (BaseβπΆ) β§ π₯ β (BaseβπΆ))) |
49 | | eleq1w 2817 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (π¦ β (BaseβπΆ) β π₯ β (BaseβπΆ))) |
50 | 49 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β (π₯ β (BaseβπΆ) β§ π₯ β (BaseβπΆ)))) |
51 | 50 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (π β§ (π₯ β (BaseβπΆ) β§ π₯ β (BaseβπΆ))))) |
52 | | 2fveq3 6851 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β (1st
β((1st βπ)βπ¦)) = (1st β((1st
βπ)βπ₯))) |
53 | 52 | fveq1d 6848 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β ((1st
β((1st βπ)βπ¦))βπ₯) = ((1st β((1st
βπ)βπ₯))βπ₯)) |
54 | 53 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β (πΉβ((1st
β((1st βπ)βπ¦))βπ₯)) = (πΉβ((1st
β((1st βπ)βπ₯))βπ₯))) |
55 | | id 22 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β π¦ = π₯) |
56 | 54, 55 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β ((πΉβ((1st
β((1st βπ)βπ¦))βπ₯)) = π¦ β (πΉβ((1st
β((1st βπ)βπ₯))βπ₯)) = π₯)) |
57 | 51, 56 | imbi12d 345 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (πΉβ((1st
β((1st βπ)βπ¦))βπ₯)) = π¦) β ((π β§ (π₯ β (BaseβπΆ) β§ π₯ β (BaseβπΆ))) β (πΉβ((1st
β((1st βπ)βπ₯))βπ₯)) = π₯))) |
58 | 10 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β πΆ β Cat) |
59 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β π¦ β (BaseβπΆ)) |
60 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (Hom
βπΆ) = (Hom
βπΆ) |
61 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β π₯ β (BaseβπΆ)) |
62 | 2, 21, 58, 59, 60, 61 | yon11 18161 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β ((1st
β((1st βπ)βπ¦))βπ₯) = (π₯(Hom βπΆ)π¦)) |
63 | 62 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (πΉβ((1st
β((1st βπ)βπ¦))βπ₯)) = (πΉβ(π₯(Hom βπΆ)π¦))) |
64 | | yoniso.1 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (πΉβ(π₯(Hom βπΆ)π¦)) = π¦) |
65 | 63, 64 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (πΉβ((1st
β((1st βπ)βπ¦))βπ₯)) = π¦) |
66 | 57, 65 | chvarvv 2003 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π₯ β (BaseβπΆ))) β (πΉβ((1st
β((1st βπ)βπ₯))βπ₯)) = π₯) |
67 | 48, 66 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (πΉβ((1st
β((1st βπ)βπ₯))βπ₯)) = π₯) |
68 | 67, 65 | eqeq12d 2749 |
. . . . . . 7
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β ((πΉβ((1st
β((1st βπ)βπ₯))βπ₯)) = (πΉβ((1st
β((1st βπ)βπ¦))βπ₯)) β π₯ = π¦)) |
69 | 46, 68 | imbitrid 243 |
. . . . . 6
β’ ((π β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (((1st βπ)βπ₯) = ((1st βπ)βπ¦) β π₯ = π¦)) |
70 | 69 | ralrimivva 3194 |
. . . . 5
β’ (π β βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)(((1st βπ)βπ₯) = ((1st βπ)βπ¦) β π₯ = π¦)) |
71 | | dff13 7206 |
. . . . 5
β’
((1st βπ):(BaseβπΆ)β1-1β(π Func π) β ((1st βπ):(BaseβπΆ)βΆ(π Func π) β§ βπ₯ β (BaseβπΆ)βπ¦ β (BaseβπΆ)(((1st βπ)βπ₯) = ((1st βπ)βπ¦) β π₯ = π¦))) |
72 | 34, 70, 71 | sylanbrc 584 |
. . . 4
β’ (π β (1st
βπ):(BaseβπΆ)β1-1β(π Func π)) |
73 | | f1f1orn 6799 |
. . . 4
β’
((1st βπ):(BaseβπΆ)β1-1β(π Func π) β (1st βπ):(BaseβπΆ)β1-1-ontoβran
(1st βπ)) |
74 | 72, 73 | syl 17 |
. . 3
β’ (π β (1st
βπ):(BaseβπΆ)β1-1-ontoβran
(1st βπ)) |
75 | 34 | frnd 6680 |
. . . . 5
β’ (π β ran (1st
βπ) β (π Func π)) |
76 | 22, 31 | ressbas2 17128 |
. . . . 5
β’ (ran
(1st βπ)
β (π Func π) β ran (1st
βπ) =
(BaseβπΈ)) |
77 | 75, 76 | syl 17 |
. . . 4
β’ (π β ran (1st
βπ) =
(BaseβπΈ)) |
78 | 77 | f1oeq3d 6785 |
. . 3
β’ (π β ((1st
βπ):(BaseβπΆ)β1-1-ontoβran
(1st βπ)
β (1st βπ):(BaseβπΆ)β1-1-ontoβ(BaseβπΈ))) |
79 | 74, 78 | mpbid 231 |
. 2
β’ (π β (1st
βπ):(BaseβπΆ)β1-1-ontoβ(BaseβπΈ)) |
80 | | eqid 2733 |
. . 3
β’
(BaseβπΈ) =
(BaseβπΈ) |
81 | | yoniso.eb |
. . 3
β’ (π β πΈ β π΅) |
82 | | yoniso.i |
. . 3
β’ πΌ = (Isoβπ·) |
83 | 3, 4, 21, 80, 5, 9, 81, 82 | catciso 18005 |
. 2
β’ (π β (π β (πΆπΌπΈ) β (π β ((πΆ Full πΈ) β© (πΆ Faith πΈ)) β§ (1st βπ):(BaseβπΆ)β1-1-ontoβ(BaseβπΈ)))) |
84 | 43, 79, 83 | mpbir2and 712 |
1
β’ (π β π β (πΆπΌπΈ)) |