Step | Hyp | Ref
| Expression |
1 | | catcoppccl.3 |
. . . . 5
β’ (π β π β π΅) |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
3 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπ) = (Hom
βπ) |
4 | | eqid 2733 |
. . . . . 6
β’
(compβπ) =
(compβπ) |
5 | | catcoppccl.o |
. . . . . 6
β’ π = (oppCatβπ) |
6 | 2, 3, 4, 5 | oppcval 17598 |
. . . . 5
β’ (π β π΅ β π = ((π sSet β¨(Hom βndx), tpos (Hom
βπ)β©) sSet
β¨(compβndx), (π₯
β ((Baseβπ)
Γ (Baseβπ)),
π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)))β©)) |
7 | 1, 6 | syl 17 |
. . . 4
β’ (π β π = ((π sSet β¨(Hom βndx), tpos (Hom
βπ)β©) sSet
β¨(compβndx), (π₯
β ((Baseβπ)
Γ (Baseβπ)),
π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)))β©)) |
8 | | catcoppccl.1 |
. . . . 5
β’ (π β π β WUni) |
9 | | catcoppccl.c |
. . . . . . . . 9
β’ πΆ = (CatCatβπ) |
10 | | catcoppccl.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΆ) |
11 | 9, 10, 8 | catcbas 17992 |
. . . . . . . 8
β’ (π β π΅ = (π β© Cat)) |
12 | 1, 11 | eleqtrd 2836 |
. . . . . . 7
β’ (π β π β (π β© Cat)) |
13 | 12 | elin1d 4159 |
. . . . . 6
β’ (π β π β π) |
14 | | df-hom 17162 |
. . . . . . . 8
β’ Hom =
Slot ;14 |
15 | | catcoppccl.2 |
. . . . . . . . 9
β’ (π β Ο β π) |
16 | 8, 15 | wunndx 17072 |
. . . . . . . 8
β’ (π β ndx β π) |
17 | 14, 8, 16 | wunstr 17065 |
. . . . . . 7
β’ (π β (Hom βndx) β
π) |
18 | 14, 8, 13 | wunstr 17065 |
. . . . . . . 8
β’ (π β (Hom βπ) β π) |
19 | 8, 18 | wuntpos 10675 |
. . . . . . 7
β’ (π β tpos (Hom βπ) β π) |
20 | 8, 17, 19 | wunop 10663 |
. . . . . 6
β’ (π β β¨(Hom βndx),
tpos (Hom βπ)β©
β π) |
21 | 8, 13, 20 | wunsets 17054 |
. . . . 5
β’ (π β (π sSet β¨(Hom βndx), tpos (Hom
βπ)β©) β
π) |
22 | | df-cco 17163 |
. . . . . . 7
β’ comp =
Slot ;15 |
23 | 22, 8, 16 | wunstr 17065 |
. . . . . 6
β’ (π β (compβndx) β
π) |
24 | | df-base 17089 |
. . . . . . . . . 10
β’ Base =
Slot 1 |
25 | 24, 8, 13 | wunstr 17065 |
. . . . . . . . 9
β’ (π β (Baseβπ) β π) |
26 | 8, 25, 25 | wunxp 10665 |
. . . . . . . 8
β’ (π β ((Baseβπ) Γ (Baseβπ)) β π) |
27 | 8, 26, 25 | wunxp 10665 |
. . . . . . 7
β’ (π β (((Baseβπ) Γ (Baseβπ)) Γ (Baseβπ)) β π) |
28 | 22, 8, 13 | wunstr 17065 |
. . . . . . . . . . . . . 14
β’ (π β (compβπ) β π) |
29 | 8, 28 | wunrn 10670 |
. . . . . . . . . . . . 13
β’ (π β ran (compβπ) β π) |
30 | 8, 29 | wununi 10647 |
. . . . . . . . . . . 12
β’ (π β βͺ ran (compβπ) β π) |
31 | 8, 30 | wundm 10669 |
. . . . . . . . . . 11
β’ (π β dom βͺ ran (compβπ) β π) |
32 | 8, 31 | wuncnv 10671 |
. . . . . . . . . 10
β’ (π β β‘dom βͺ ran
(compβπ) β π) |
33 | 8 | wun0 10659 |
. . . . . . . . . . 11
β’ (π β β
β π) |
34 | 8, 33 | wunsn 10657 |
. . . . . . . . . 10
β’ (π β {β
} β π) |
35 | 8, 32, 34 | wunun 10651 |
. . . . . . . . 9
β’ (π β (β‘dom βͺ ran
(compβπ) βͺ
{β
}) β π) |
36 | 8, 30 | wunrn 10670 |
. . . . . . . . 9
β’ (π β ran βͺ ran (compβπ) β π) |
37 | 8, 35, 36 | wunxp 10665 |
. . . . . . . 8
β’ (π β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) β π) |
38 | 8, 37 | wunpw 10648 |
. . . . . . 7
β’ (π β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) β π) |
39 | | tposssxp 8162 |
. . . . . . . . . . . 12
β’ tpos
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β ((β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) Γ ran (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) |
40 | | ovssunirn 7394 |
. . . . . . . . . . . . . . 15
β’
(β¨π¦,
(2nd βπ₯)β©(compβπ)(1st βπ₯)) β βͺ ran
(compβπ) |
41 | | dmss 5859 |
. . . . . . . . . . . . . . 15
β’
((β¨π¦,
(2nd βπ₯)β©(compβπ)(1st βπ₯)) β βͺ ran
(compβπ) β dom
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β dom βͺ
ran (compβπ)) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ dom
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β dom βͺ
ran (compβπ) |
43 | | cnvss 5829 |
. . . . . . . . . . . . . 14
β’ (dom
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β dom βͺ
ran (compβπ) β
β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β β‘dom βͺ ran
(compβπ)) |
44 | | unss1 4140 |
. . . . . . . . . . . . . 14
β’ (β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β β‘dom βͺ ran
(compβπ) β
(β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) β (β‘dom βͺ ran
(compβπ) βͺ
{β
})) |
45 | 42, 43, 44 | mp2b 10 |
. . . . . . . . . . . . 13
β’ (β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) β (β‘dom βͺ ran
(compβπ) βͺ
{β
}) |
46 | 40 | rnssi 5896 |
. . . . . . . . . . . . 13
β’ ran
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β ran βͺ
ran (compβπ) |
47 | | xpss12 5649 |
. . . . . . . . . . . . 13
β’ (((β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) β (β‘dom βͺ ran
(compβπ) βͺ
{β
}) β§ ran (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β ran βͺ
ran (compβπ)) β
((β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) Γ ran (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
48 | 45, 46, 47 | mp2an 691 |
. . . . . . . . . . . 12
β’ ((β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) Γ ran (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) |
49 | 39, 48 | sstri 3954 |
. . . . . . . . . . 11
β’ tpos
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) |
50 | | elpw2g 5302 |
. . . . . . . . . . . 12
β’ (((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) β π β (tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) β tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)))) |
51 | 37, 50 | syl 17 |
. . . . . . . . . . 11
β’ (π β (tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) β tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)))) |
52 | 49, 51 | mpbiri 258 |
. . . . . . . . . 10
β’ (π β tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
53 | 52 | ralrimivw 3144 |
. . . . . . . . 9
β’ (π β βπ¦ β (Baseβπ)tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
54 | 53 | ralrimivw 3144 |
. . . . . . . 8
β’ (π β βπ₯ β ((Baseβπ) Γ (Baseβπ))βπ¦ β (Baseβπ)tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
55 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β ((Baseβπ) Γ (Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) = (π₯ β ((Baseβπ) Γ (Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) |
56 | 55 | fmpo 8001 |
. . . . . . . 8
β’
(βπ₯ β
((Baseβπ) Γ
(Baseβπ))βπ¦ β (Baseβπ)tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) β (π₯ β ((Baseβπ) Γ (Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))):(((Baseβπ) Γ (Baseβπ)) Γ (Baseβπ))βΆπ« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
57 | 54, 56 | sylib 217 |
. . . . . . 7
β’ (π β (π₯ β ((Baseβπ) Γ (Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))):(((Baseβπ) Γ (Baseβπ)) Γ (Baseβπ))βΆπ« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
58 | 8, 27, 38, 57 | wunf 10668 |
. . . . . 6
β’ (π β (π₯ β ((Baseβπ) Γ (Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) β π) |
59 | 8, 23, 58 | wunop 10663 |
. . . . 5
β’ (π β β¨(compβndx),
(π₯ β
((Baseβπ) Γ
(Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)))β© β π) |
60 | 8, 21, 59 | wunsets 17054 |
. . . 4
β’ (π β ((π sSet β¨(Hom βndx), tpos (Hom
βπ)β©) sSet
β¨(compβndx), (π₯
β ((Baseβπ)
Γ (Baseβπ)),
π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)))β©) β π) |
61 | 7, 60 | eqeltrd 2834 |
. . 3
β’ (π β π β π) |
62 | 12 | elin2d 4160 |
. . . 4
β’ (π β π β Cat) |
63 | 5 | oppccat 17609 |
. . . 4
β’ (π β Cat β π β Cat) |
64 | 62, 63 | syl 17 |
. . 3
β’ (π β π β Cat) |
65 | 61, 64 | elind 4155 |
. 2
β’ (π β π β (π β© Cat)) |
66 | 65, 11 | eleqtrrd 2837 |
1
β’ (π β π β π΅) |