Theorem rescabsOLD

Description: Obsolete version of seqp1d as of 10-Nov-2024. Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	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	rescabsOLD	|- ( 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		1re	|- 1 e. RR
16		1nn	|- 1 e. NN
17		4nn0	|- 4 e. NN0
18		1nn0	|- 1 e. NN0
19		1lt10	|- 1 < ; 1 0
20	16 17 18 19	declti	|- 1 < ; 1 4
21	15 20	ltneii	|- 1 =/= ; 1 4
22		basendx	|- ( Base ` ndx ) = 1
23		homndx	|- ( Hom ` ndx ) = ; 1 4
24	22 23	neeq12i	|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) <-> 1 =/= ; 1 4 )
25	21 24	mpbir	|- ( Base ` ndx ) =/= ( Hom ` ndx )
26	14 25	setsnid	|- ( Base ` ( C |`s S ) ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
27	13 26	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 >. ) )
28	10 11 12 27	syl3anc	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
29	28	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 >. ) )
30		ovex	|- ( C |`s S ) e. _V
31	8 8	xpexd	|- ( ph -> ( T X. T ) e. _V )
32		fnex	|- ( ( J Fn ( T X. T ) /\ ( T X. T ) e. _V ) -> J e. _V )
33	3 31 32	syl2anc	|- ( ph -> J e. _V )
34	33	adantr	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> J e. _V )
35		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 >. ) )
36	30 34 35	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 >. ) )
37		eqid	|- ( C |`s S ) = ( C |`s S )
38		eqid	|- ( Base ` C ) = ( Base ` C )
39	37 38	ressbas	|- ( S e. W -> ( S i^i ( Base ` C ) ) = ( Base ` ( C |`s S ) ) )
40	4 39	syl	|- ( ph -> ( S i^i ( Base ` C ) ) = ( Base ` ( C |`s S ) ) )
41	40	sseq1d	|- ( ph -> ( ( S i^i ( Base ` C ) ) C_ T <-> ( Base ` ( C |`s S ) ) C_ T ) )
42	41	biimpar	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ T )
43		inss2	|- ( S i^i ( Base ` C ) ) C_ ( Base ` C )
44	43	a1i	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ ( Base ` C ) )
45	42 44	ssind	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) C_ ( T i^i ( Base ` C ) ) )
46	5	adantr	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> T C_ S )
47	46	ssrind	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( T i^i ( Base ` C ) ) C_ ( S i^i ( Base ` C ) ) )
48	45 47	eqssd	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( S i^i ( Base ` C ) ) = ( T i^i ( Base ` C ) ) )
49	48	oveq2d	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s ( S i^i ( Base ` C ) ) ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
50	4	adantr	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> S e. W )
51	38	ressinbas	|- ( S e. W -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
52	50 51	syl	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
53	38	ressinbas	|- ( T e. _V -> ( C |`s T ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
54	12 53	syl	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s T ) = ( C |`s ( T i^i ( Base ` C ) ) ) )
55	49 52 54	3eqtr4d	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) = ( C |`s T ) )
56	55	oveq1d	|- ( ( ph /\ ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
57	29 36 56	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 >. ) )
58		simpr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> -. ( Base ` ( C |`s S ) ) C_ T )
59		ovexd	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) e. _V )
60	8	adantr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> T e. _V )
61	13 26	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 ) ) ) >. ) )
62	58 59 60 61	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 ) ) ) >. ) )
63		ovexd	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( C |`s S ) e. _V )
64	25	necomi	|- ( Hom ` ndx ) =/= ( Base ` ndx )
65	64	a1i	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( Hom ` ndx ) =/= ( Base ` ndx ) )
66	4 4	xpexd	|- ( ph -> ( S X. S ) e. _V )
67		fnex	|- ( ( H Fn ( S X. S ) /\ ( S X. S ) e. _V ) -> H e. _V )
68	2 66 67	syl2anc	|- ( ph -> H e. _V )
69	68	adantr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> H e. _V )
70		fvex	|- ( Base ` ( C |`s S ) ) e. _V
71	70	inex2	|- ( T i^i ( Base ` ( C |`s S ) ) ) e. _V
72	71	a1i	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( T i^i ( Base ` ( C |`s S ) ) ) e. _V )
73		fvex	|- ( Hom ` ndx ) e. _V
74		fvex	|- ( Base ` ndx ) e. _V
75	73 74	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 >. ) )
76	63 65 69 72 75	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 >. ) )
77		eqid	|- ( ( C |`s S ) |`s T ) = ( ( C |`s S ) |`s T )
78		eqid	|- ( Base ` ( C |`s S ) ) = ( Base ` ( C |`s S ) )
79	77 78	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 ) ) ) >. ) )
80	58 63 60 79	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 ) ) ) >. ) )
81	4	adantr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> S e. W )
82	5	adantr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> T C_ S )
83		ressabs	|- ( ( S e. W /\ T C_ S ) -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
84	81 82 83	syl2anc	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) |`s T ) = ( C |`s T ) )
85	80 84	eqtr3d	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( C |`s S ) sSet <. ( Base ` ndx ) , ( T i^i ( Base ` ( C |`s S ) ) ) >. ) = ( C |`s T ) )
86	85	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 >. ) )
87	62 76 86	3eqtrd	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , H >. ) )
88	87	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 >. ) )
89		ovex	|- ( C |`s T ) e. _V
90	33	adantr	|- ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> J e. _V )
91		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 >. ) )
92	89 90 91	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 >. ) )
93	88 92	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 >. ) )
94	57 93	pm2.61dan	|- ( ph -> ( ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`s T ) sSet <. ( Hom ` ndx ) , J >. ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
95	9 94	eqtrd	|- ( ph -> ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
96		eqid	|- ( C |`cat H ) = ( C |`cat H )
97	96 1 4 2	rescval2	|- ( ph -> ( C |`cat H ) = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
98	97	oveq1d	|- ( ph -> ( ( C |`cat H ) |`cat J ) = ( ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) |`cat J ) )
99		eqid	|- ( C |`cat J ) = ( C |`cat J )
100	99 1 8 3	rescval2	|- ( ph -> ( C |`cat J ) = ( ( C |`s T ) sSet <. ( Hom ` ndx ) , J >. ) )
101	95 98 100	3eqtr4d	|- ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) )