Theorem rescabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 9-Nov-2024)

	Ref	Expression
Hypotheses	rescabs.c	|- ( ph -> C e. V )
	rescabs.h	|- ( ph -> H Fn ( S X. S ) )
	rescabs.j	|- ( ph -> J Fn ( T X. T ) )
	rescabs.s	|- ( ph -> S e. W )
	rescabs.t	|- ( ph -> T C_ S )
Assertion	rescabs	|- ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) )

Proof

Step	Hyp	Ref	Expression
1		rescabs.c	|- ( ph -> C e. V )
2		rescabs.h	|- ( ph -> H Fn ( S X. S ) )
3		rescabs.j	|- ( ph -> J Fn ( T X. T ) )
4		rescabs.s	|- ( ph -> S e. W )
5		rescabs.t	|- ( ph -> T C_ S )
6		eqid	|- ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J )
7		ovexd	|- ( ph -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
8	4 5	ssexd	|- ( ph -> T e. _V )
9	6 7 8 3	rescval2	|- ( ph -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
10		simpr	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( Base ` ( C |`s S ) ) C_ T )
11		ovexd	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
12	8	adantr	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> T e. _V )
13		eqid	|- ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T )
14		baseid	|- Base = Slot ( Base ` ndx )
15		slotsbhcdif	|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
16	15	simp1i	|- ( Base ` ndx ) =/= ( Hom ` ndx )
17	14 16	setsnid	|- ( Base ` ( C |`s S ) ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
18	13 17	ressid2	|- ( ( ( Base ` ( C |`s S ) ) C_ T /\ ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V /\ T e. _V ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
19	10 11 12 18	syl3anc	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
20	19	oveq1d	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) )
21		ovex	|- ( C |`s S ) e. _V
22	8 8	xpexd	|- ( ph -> ( T X. T ) e. _V )
23	3 22	fnexd	|- ( ph -> J e. _V )
24	23	adantr	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> J e. _V )
25		setsabs	|- ( ( ( C |`s S ) e. _V /\ J e. _V ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) )
26	21 24 25	sylancr	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) )
27		eqid	|- ( C |`s S ) = ( C |`s S )
28		eqid	|- ( Base ` C ) = ( Base ` C )
29	27 28	ressbas	|- ( S e. W -> ( S i^i ( Base ` C ) ) = ( Base ` ( C |`s S ) ) )
30	4 29	syl	|- ( ph -> ( S i^i ( Base ` C ) ) = ( Base ` ( C |`s S ) ) )
31	30	sseq1d	|- ( ph -> ( ( S i^i ( Base ` C ) ) C_ T <-> ( Base ` ( C |`s S ) ) C_ T ) )
32	31	biimpar	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ T )
33		inss2	|- ( S i^i ( Base ` C ) ) C_ ( Base ` C )
34	33	a1i	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ ( Base ` C ) )
35	32 34	ssind	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ ( T i^i ( Base ` C ) ) )
36	5	adantr	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> T C_ S )
37	36	ssrind	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( T i^i ( Base ` C ) ) C_ ( S i^i ( Base ` C ) ) )
38	35 37	eqssd	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) = ( T i^i ( Base ` C ) ) )
39	38	oveq2d	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s ( S i^i ( Base ` C ) ) ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
40	4	adantr	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> S e. W )
41	28	ressinbas	|- ( S e. W -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
42	40 41	syl	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
43	28	ressinbas	|- ( T e. _V -> ( C |`s T ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
44	12 43	syl	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s T ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
45	39 42 44	3eqtr4d	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) = ( C |`s T ) )
46	45	oveq1d	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
47	20 26 46	3eqtrd	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
48		simpr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> -. ( Base ` ( C |`s S ) ) C_ T )
49		ovexd	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
50	8	adantr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> T e. _V )
51	13 17	ressval2	|- ( ( -. ( Base ` ( C |`s S ) ) C_ T /\ ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V /\ T e. _V ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
52	48 49 50 51	syl3anc	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
53		ovexd	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) e. _V )
54	16	necomi	|- ( Hom ` ndx ) =/= ( Base ` ndx )
55	54	a1i	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( Hom ` ndx ) =/= ( Base ` ndx ) )
56	4 4	xpexd	|- ( ph -> ( S X. S ) e. _V )
57	2 56	fnexd	|- ( ph -> H e. _V )
58	57	adantr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> H e. _V )
59		fvex	|- ( Base ` ( C |`s S ) ) e. _V
60	59	inex2	|- ( T i^i ( Base ` ( C |`s S ) ) ) e. _V
61	60	a1i	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( T i^i ( Base ` ( C |`s S ) ) ) e. _V )
62		fvex	|- ( Hom ` ndx ) e. _V
63		fvex	|- ( Base ` ndx ) e. _V
64	62 63	setscom	|- ( ( ( ( C |`s S ) e. _V /\ ( Hom ` ndx ) =/= ( Base ` ndx ) ) /\ ( H e. _V /\ ( T i^i ( Base ` ( C |`s S ) ) ) e. _V ) ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) sSet <. ( Hom ` ndx ) , H >. ) )
65	53 55 58 61 64	syl22anc	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) sSet <. ( Hom ` ndx ) , H >. ) )
66		eqid	|- ( ( C |`s S ) |`s T ) = ( ( C |`s S ) |`s T )
67		eqid	|- ( Base ` ( C |`s S ) ) = ( Base ` ( C |`s S ) )
68	66 67	ressval2	|- ( ( -. ( Base ` ( C |`s S ) ) C_ T /\ ( C |`s S ) e. _V /\ T e. _V ) -> ( ( C |`s S ) |`s T ) = ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
69	48 53 50 68	syl3anc	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) |`s T ) = ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) )
70	5	adantr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> T C_ S )
71		ressabs	|- ( ( S e. W /\ T C_ S ) -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
72	4 70 71	syl2an2r	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
73	69 72	eqtr3d	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( C |`s T ) )
74	73	oveq1d	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) sSet <. ( Hom ` ndx ) , H >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) )
75	52 65 74	3eqtrd	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) )
76	75	oveq1d	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) )
77		ovex	|- ( C |`s T ) e. _V
78	23	adantr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> J e. _V )
79		setsabs	|- ( ( ( C |`s T ) e. _V /\ J e. _V ) -> ( ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
80	77 78 79	sylancr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
81	76 80	eqtrd	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
82	47 81	pm2.61dan	|- ( ph -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
83	9 82	eqtrd	|- ( ph -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
84		eqid	|- ( C |`cat H ) = ( C |`cat H )
85	84 1 4 2	rescval2	|- ( ph -> ( C |`cat H ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
86	85	oveq1d	|- ( ph -> ( ( C |`cat H ) |`cat J ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) )
87		eqid	|- ( C |`cat J ) = ( C |`cat J )
88	87 1 8 3	rescval2	|- ( ph -> ( C |`cat J ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
89	83 86 88	3eqtr4d	|- ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) )