Step | Hyp | Ref
| Expression |
1 | | postc.c |
. . . 4
β’ (π β πΆ = (ProsetToCatβπΎ)) |
2 | | postc.k |
. . . 4
β’ (π β πΎ β Proset ) |
3 | 1, 2 | prstcprs 47181 |
. . 3
β’ (π β πΆ β Proset ) |
4 | | postc.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
5 | | eqid 2733 |
. . . . 5
β’
(leβπΆ) =
(leβπΆ) |
6 | 4, 5 | ispos2 18209 |
. . . 4
β’ (πΆ β Poset β (πΆ β Proset β§
βπ₯ β π΅ βπ¦ β π΅ ((π₯(leβπΆ)π¦ β§ π¦(leβπΆ)π₯) β π₯ = π¦))) |
7 | 6 | baib 537 |
. . 3
β’ (πΆ β Proset β (πΆ β Poset β
βπ₯ β π΅ βπ¦ β π΅ ((π₯(leβπΆ)π¦ β§ π¦(leβπΆ)π₯) β π₯ = π¦))) |
8 | 3, 7 | syl 17 |
. 2
β’ (π β (πΆ β Poset β βπ₯ β π΅ βπ¦ β π΅ ((π₯(leβπΆ)π¦ β§ π¦(leβπΆ)π₯) β π₯ = π¦))) |
9 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΆ = (ProsetToCatβπΎ)) |
10 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΎ β Proset ) |
11 | 9, 10 | prstcthin 47182 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΆ β ThinCat) |
12 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯ β π΅) |
13 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦ β π΅) |
14 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπΆ) = (Hom
βπΆ) |
15 | 11, 4, 12, 13, 14 | thinccic 47167 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯( βπ βπΆ)π¦ β ((π₯(Hom βπΆ)π¦) β β
β§ (π¦(Hom βπΆ)π₯) β β
))) |
16 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (leβπΆ) = (leβπΆ)) |
17 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (Hom βπΆ) = (Hom βπΆ)) |
18 | 12, 4 | eleqtrdi 2844 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π₯ β (BaseβπΆ)) |
19 | 13, 4 | eleqtrdi 2844 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π¦ β (BaseβπΆ)) |
20 | 9, 10, 16, 17, 18, 19 | prstchom 47183 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(leβπΆ)π¦ β (π₯(Hom βπΆ)π¦) β β
)) |
21 | 9, 10, 16, 17, 19, 18 | prstchom 47183 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π¦(leβπΆ)π₯ β (π¦(Hom βπΆ)π₯) β β
)) |
22 | 20, 21 | anbi12d 632 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π₯(leβπΆ)π¦ β§ π¦(leβπΆ)π₯) β ((π₯(Hom βπΆ)π¦) β β
β§ (π¦(Hom βπΆ)π₯) β β
))) |
23 | 15, 22 | bitr4d 282 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯( βπ βπΆ)π¦ β (π₯(leβπΆ)π¦ β§ π¦(leβπΆ)π₯))) |
24 | 23 | imbi1d 342 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π₯( βπ βπΆ)π¦ β π₯ = π¦) β ((π₯(leβπΆ)π¦ β§ π¦(leβπΆ)π₯) β π₯ = π¦))) |
25 | 24 | 2ralbidva 3207 |
. 2
β’ (π β (βπ₯ β π΅ βπ¦ β π΅ (π₯( βπ βπΆ)π¦ β π₯ = π¦) β βπ₯ β π΅ βπ¦ β π΅ ((π₯(leβπΆ)π¦ β§ π¦(leβπΆ)π₯) β π₯ = π¦))) |
26 | 8, 25 | bitr4d 282 |
1
β’ (π β (πΆ β Poset β βπ₯ β π΅ βπ¦ β π΅ (π₯( βπ βπΆ)π¦ β π₯ = π¦))) |