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 |
. . . . . . 7
β’ πΆ = (CatCatβπ) |
10 | | catcoppccl.b |
. . . . . . 7
β’ π΅ = (BaseβπΆ) |
11 | 9, 10, 8, 1 | catcbascl 18003 |
. . . . . 6
β’ (π β π β π) |
12 | | homid 17298 |
. . . . . . . 8
β’ Hom =
Slot (Hom βndx) |
13 | | catcoppccl.2 |
. . . . . . . . 9
β’ (π β Ο β π) |
14 | 8, 13 | wunndx 17072 |
. . . . . . . 8
β’ (π β ndx β π) |
15 | 12, 8, 14 | wunstr 17065 |
. . . . . . 7
β’ (π β (Hom βndx) β
π) |
16 | 9, 10, 8, 1 | catchomcl 18006 |
. . . . . . . 8
β’ (π β (Hom βπ) β π) |
17 | 8, 16 | wuntpos 10675 |
. . . . . . 7
β’ (π β tpos (Hom βπ) β π) |
18 | 8, 15, 17 | wunop 10663 |
. . . . . 6
β’ (π β β¨(Hom βndx),
tpos (Hom βπ)β©
β π) |
19 | 8, 11, 18 | wunsets 17054 |
. . . . 5
β’ (π β (π sSet β¨(Hom βndx), tpos (Hom
βπ)β©) β
π) |
20 | | ccoid 17300 |
. . . . . . 7
β’ comp =
Slot (compβndx) |
21 | 20, 8, 14 | wunstr 17065 |
. . . . . 6
β’ (π β (compβndx) β
π) |
22 | 9, 10, 8, 1 | catcbaselcl 18005 |
. . . . . . . . 9
β’ (π β (Baseβπ) β π) |
23 | 8, 22, 22 | wunxp 10665 |
. . . . . . . 8
β’ (π β ((Baseβπ) Γ (Baseβπ)) β π) |
24 | 8, 23, 22 | wunxp 10665 |
. . . . . . 7
β’ (π β (((Baseβπ) Γ (Baseβπ)) Γ (Baseβπ)) β π) |
25 | 9, 10, 8, 1 | catcccocl 18007 |
. . . . . . . . . . . . . 14
β’ (π β (compβπ) β π) |
26 | 8, 25 | wunrn 10670 |
. . . . . . . . . . . . 13
β’ (π β ran (compβπ) β π) |
27 | 8, 26 | wununi 10647 |
. . . . . . . . . . . 12
β’ (π β βͺ ran (compβπ) β π) |
28 | 8, 27 | wundm 10669 |
. . . . . . . . . . 11
β’ (π β dom βͺ ran (compβπ) β π) |
29 | 8, 28 | wuncnv 10671 |
. . . . . . . . . 10
β’ (π β β‘dom βͺ ran
(compβπ) β π) |
30 | 8 | wun0 10659 |
. . . . . . . . . . 11
β’ (π β β
β π) |
31 | 8, 30 | wunsn 10657 |
. . . . . . . . . 10
β’ (π β {β
} β π) |
32 | 8, 29, 31 | wunun 10651 |
. . . . . . . . 9
β’ (π β (β‘dom βͺ ran
(compβπ) βͺ
{β
}) β π) |
33 | 8, 27 | wunrn 10670 |
. . . . . . . . 9
β’ (π β ran βͺ ran (compβπ) β π) |
34 | 8, 32, 33 | wunxp 10665 |
. . . . . . . 8
β’ (π β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) β π) |
35 | 8, 34 | wunpw 10648 |
. . . . . . 7
β’ (π β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) β π) |
36 | | tposssxp 8162 |
. . . . . . . . . . . 12
β’ tpos
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β ((β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) Γ ran (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) |
37 | | ovssunirn 7394 |
. . . . . . . . . . . . . . 15
β’
(β¨π¦,
(2nd βπ₯)β©(compβπ)(1st βπ₯)) β βͺ ran
(compβπ) |
38 | | dmss 5859 |
. . . . . . . . . . . . . . 15
β’
((β¨π¦,
(2nd βπ₯)β©(compβπ)(1st βπ₯)) β βͺ ran
(compβπ) β dom
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β dom βͺ
ran (compβπ)) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ dom
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β dom βͺ
ran (compβπ) |
40 | | cnvss 5829 |
. . . . . . . . . . . . . 14
β’ (dom
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β dom βͺ
ran (compβπ) β
β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β β‘dom βͺ ran
(compβπ)) |
41 | | unss1 4140 |
. . . . . . . . . . . . . 14
β’ (β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β β‘dom βͺ ran
(compβπ) β
(β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) β (β‘dom βͺ ran
(compβπ) βͺ
{β
})) |
42 | 39, 40, 41 | mp2b 10 |
. . . . . . . . . . . . 13
β’ (β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) β (β‘dom βͺ ran
(compβπ) βͺ
{β
}) |
43 | 37 | rnssi 5896 |
. . . . . . . . . . . . 13
β’ ran
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β ran βͺ
ran (compβπ) |
44 | | 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βπ))) |
45 | 42, 43, 44 | mp2an 691 |
. . . . . . . . . . . 12
β’ ((β‘dom (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) βͺ {β
}) Γ ran (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) |
46 | 36, 45 | sstri 3954 |
. . . . . . . . . . 11
β’ tpos
(β¨π¦, (2nd
βπ₯)β©(compβπ)(1st βπ₯)) β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) |
47 | | 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βπ)))) |
48 | 34, 47 | syl 17 |
. . . . . . . . . . 11
β’ (π β (tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)) β tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ)))) |
49 | 46, 48 | mpbiri 258 |
. . . . . . . . . 10
β’ (π β tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
50 | 49 | ralrimivw 3144 |
. . . . . . . . 9
β’ (π β βπ¦ β (Baseβπ)tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
51 | 50 | ralrimivw 3144 |
. . . . . . . 8
β’ (π β βπ₯ β ((Baseβπ) Γ (Baseβπ))βπ¦ β (Baseβπ)tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)) β π« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
52 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β ((Baseβπ) Γ (Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) = (π₯ β ((Baseβπ) Γ (Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) |
53 | 52 | 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βπ))) |
54 | 51, 53 | sylib 217 |
. . . . . . 7
β’ (π β (π₯ β ((Baseβπ) Γ (Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))):(((Baseβπ) Γ (Baseβπ)) Γ (Baseβπ))βΆπ« ((β‘dom βͺ ran
(compβπ) βͺ
{β
}) Γ ran βͺ ran (compβπ))) |
55 | 8, 24, 35, 54 | wunf 10668 |
. . . . . 6
β’ (π β (π₯ β ((Baseβπ) Γ (Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯))) β π) |
56 | 8, 21, 55 | wunop 10663 |
. . . . 5
β’ (π β β¨(compβndx),
(π₯ β
((Baseβπ) Γ
(Baseβπ)), π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)))β© β π) |
57 | 8, 19, 56 | wunsets 17054 |
. . . 4
β’ (π β ((π sSet β¨(Hom βndx), tpos (Hom
βπ)β©) sSet
β¨(compβndx), (π₯
β ((Baseβπ)
Γ (Baseβπ)),
π¦ β (Baseβπ) β¦ tpos (β¨π¦, (2nd βπ₯)β©(compβπ)(1st βπ₯)))β©) β π) |
58 | 7, 57 | eqeltrd 2834 |
. . 3
β’ (π β π β π) |
59 | 9, 10, 8 | catcbas 17992 |
. . . . . 6
β’ (π β π΅ = (π β© Cat)) |
60 | 1, 59 | eleqtrd 2836 |
. . . . 5
β’ (π β π β (π β© Cat)) |
61 | 60 | elin2d 4160 |
. . . 4
β’ (π β π β Cat) |
62 | 5 | oppccat 17609 |
. . . 4
β’ (π β Cat β π β Cat) |
63 | 61, 62 | syl 17 |
. . 3
β’ (π β π β Cat) |
64 | 58, 63 | elind 4155 |
. 2
β’ (π β π β (π β© Cat)) |
65 | 64, 59 | eleqtrrd 2837 |
1
β’ (π β π β π΅) |