Step | Hyp | Ref
| Expression |
1 | | indthinc.b |
. 2
β’ (π β π΅ = (BaseβπΆ)) |
2 | | prsthinc.h |
. 2
β’ (π β ( β€ Γ
{1o}) = (Hom βπΆ)) |
3 | | eqidd 2734 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ( β€ Γ
{1o}) = ( β€ Γ
{1o})) |
4 | 3 | f1omo 47013 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β β*π π β (( β€ Γ
{1o})ββ¨π₯, π¦β©)) |
5 | | df-ov 7361 |
. . . . 5
β’ (π₯( β€ Γ
{1o})π¦) = ((
β€
Γ {1o})ββ¨π₯, π¦β©) |
6 | 5 | eleq2i 2826 |
. . . 4
β’ (π β (π₯( β€ Γ
{1o})π¦) β
π β (( β€ Γ
{1o})ββ¨π₯, π¦β©)) |
7 | 6 | mobii 2543 |
. . 3
β’
(β*π π β (π₯( β€ Γ
{1o})π¦) β
β*π π β (( β€ Γ
{1o})ββ¨π₯, π¦β©)) |
8 | 4, 7 | sylibr 233 |
. 2
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β β*π π β (π₯( β€ Γ
{1o})π¦)) |
9 | | prsthinc.o |
. 2
β’ (π β β
=
(compβπΆ)) |
10 | | prsthinc.p |
. 2
β’ (π β πΆ β Proset ) |
11 | | biid 261 |
. 2
β’ (((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))) β
((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§)))) |
12 | | 0lt1o 8451 |
. . 3
β’ β
β 1o |
13 | 1 | eleq2d 2820 |
. . . . . 6
β’ (π β (π¦ β π΅ β π¦ β (BaseβπΆ))) |
14 | | eqid 2733 |
. . . . . . . 8
β’
(BaseβπΆ) =
(BaseβπΆ) |
15 | | eqid 2733 |
. . . . . . . 8
β’
(leβπΆ) =
(leβπΆ) |
16 | 14, 15 | prsref 18193 |
. . . . . . 7
β’ ((πΆ β Proset β§ π¦ β (BaseβπΆ)) β π¦(leβπΆ)π¦) |
17 | 10, 16 | sylan 581 |
. . . . . 6
β’ ((π β§ π¦ β (BaseβπΆ)) β π¦(leβπΆ)π¦) |
18 | 13, 17 | sylbida 593 |
. . . . 5
β’ ((π β§ π¦ β π΅) β π¦(leβπΆ)π¦) |
19 | | prsthinc.l |
. . . . . . 7
β’ (π β β€ = (leβπΆ)) |
20 | 19 | breqd 5117 |
. . . . . 6
β’ (π β (π¦ β€ π¦ β π¦(leβπΆ)π¦)) |
21 | 20 | biimpar 479 |
. . . . 5
β’ ((π β§ π¦(leβπΆ)π¦) β π¦ β€ π¦) |
22 | 18, 21 | syldan 592 |
. . . 4
β’ ((π β§ π¦ β π΅) β π¦ β€ π¦) |
23 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π¦ β π΅) β ( β€ Γ
{1o}) = ( β€ Γ
{1o})) |
24 | | 1oex 8423 |
. . . . . 6
β’
1o β V |
25 | 24 | a1i 11 |
. . . . 5
β’ ((π β§ π¦ β π΅) β 1o β
V) |
26 | | 1n0 8435 |
. . . . . 6
β’
1o β β
|
27 | 26 | a1i 11 |
. . . . 5
β’ ((π β§ π¦ β π΅) β 1o β
β
) |
28 | 23, 25, 27 | fvconstr 47008 |
. . . 4
β’ ((π β§ π¦ β π΅) β (π¦ β€ π¦ β (π¦( β€ Γ
{1o})π¦) =
1o)) |
29 | 22, 28 | mpbid 231 |
. . 3
β’ ((π β§ π¦ β π΅) β (π¦( β€ Γ
{1o})π¦) =
1o) |
30 | 12, 29 | eleqtrrid 2841 |
. 2
β’ ((π β§ π¦ β π΅) β β
β (π¦( β€ Γ
{1o})π¦)) |
31 | | 0ov 7395 |
. . . . . 6
β’
(β¨π₯, π¦β©β
π§) = β
|
32 | 31 | oveqi 7371 |
. . . . 5
β’ (π(β¨π₯, π¦β©β
π§)π) = (πβ
π) |
33 | | 0ov 7395 |
. . . . 5
β’ (πβ
π) = β
|
34 | 32, 33 | eqtri 2761 |
. . . 4
β’ (π(β¨π₯, π¦β©β
π§)π) = β
|
35 | 34, 12 | eqeltri 2830 |
. . 3
β’ (π(β¨π₯, π¦β©β
π§)π) β 1o |
36 | | simpl 484 |
. . . . 5
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β π) |
37 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β πΆ β Proset
) |
38 | 1 | eleq2d 2820 |
. . . . . . . . 9
β’ (π β (π₯ β π΅ β π₯ β (BaseβπΆ))) |
39 | 1 | eleq2d 2820 |
. . . . . . . . 9
β’ (π β (π§ β π΅ β π§ β (BaseβπΆ))) |
40 | 38, 13, 39 | 3anbi123d 1437 |
. . . . . . . 8
β’ (π β ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ) β§ π§ β (BaseβπΆ)))) |
41 | 40 | biimpa 478 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ) β§ π§ β (BaseβπΆ))) |
42 | 41 | adantrr 716 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β (π₯ β
(BaseβπΆ) β§ π¦ β (BaseβπΆ) β§ π§ β (BaseβπΆ))) |
43 | | eqidd 2734 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β ( β€ Γ
{1o}) = ( β€ Γ
{1o})) |
44 | | simprrl 780 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β π β (π₯( β€ Γ
{1o})π¦)) |
45 | 43, 44 | fvconstr2 47010 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β π₯ β€ π¦) |
46 | 19 | breqd 5117 |
. . . . . . . 8
β’ (π β (π₯ β€ π¦ β π₯(leβπΆ)π¦)) |
47 | 46 | biimpd 228 |
. . . . . . 7
β’ (π β (π₯ β€ π¦ β π₯(leβπΆ)π¦)) |
48 | 36, 45, 47 | sylc 65 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β π₯(leβπΆ)π¦) |
49 | | simprrr 781 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β π β (π¦( β€ Γ
{1o})π§)) |
50 | 43, 49 | fvconstr2 47010 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β π¦ β€ π§) |
51 | 19 | breqd 5117 |
. . . . . . . 8
β’ (π β (π¦ β€ π§ β π¦(leβπΆ)π§)) |
52 | 51 | biimpd 228 |
. . . . . . 7
β’ (π β (π¦ β€ π§ β π¦(leβπΆ)π§)) |
53 | 36, 50, 52 | sylc 65 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β π¦(leβπΆ)π§) |
54 | 14, 15 | prstr 18194 |
. . . . . 6
β’ ((πΆ β Proset β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ) β§ π§ β (BaseβπΆ)) β§ (π₯(leβπΆ)π¦ β§ π¦(leβπΆ)π§)) β π₯(leβπΆ)π§) |
55 | 37, 42, 48, 53, 54 | syl112anc 1375 |
. . . . 5
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β π₯(leβπΆ)π§) |
56 | 19 | breqd 5117 |
. . . . . 6
β’ (π β (π₯ β€ π§ β π₯(leβπΆ)π§)) |
57 | 56 | biimprd 248 |
. . . . 5
β’ (π β (π₯(leβπΆ)π§ β π₯ β€ π§)) |
58 | 36, 55, 57 | sylc 65 |
. . . 4
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β π₯ β€ π§) |
59 | 24 | a1i 11 |
. . . . 5
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β 1o β V) |
60 | 26 | a1i 11 |
. . . . 5
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β 1o β β
) |
61 | 43, 59, 60 | fvconstr 47008 |
. . . 4
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β (π₯ β€ π§ β (π₯( β€ Γ
{1o})π§) =
1o)) |
62 | 58, 61 | mpbid 231 |
. . 3
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β (π₯( β€ Γ
{1o})π§) =
1o) |
63 | 35, 62 | eleqtrrid 2841 |
. 2
β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β§ (π β (π₯( β€ Γ
{1o})π¦) β§
π β (π¦( β€ Γ
{1o})π§))))
β (π(β¨π₯, π¦β©β
π§)π) β (π₯( β€ Γ
{1o})π§)) |
64 | 1, 2, 8, 9, 10, 11, 30, 63 | isthincd2 47144 |
1
β’ (π β (πΆ β ThinCat β§ (IdβπΆ) = (π¦ β π΅ β¦ β
))) |