# Metamath Proof Explorer

## Theorem rescabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017)

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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) ) >. ) )`
` |-  ( ( ph /\ -. ( Base ` ( C |`s S ) ) C_ T ) -> S e. W )`
` |-  ( ( 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`
` |-  ( ( 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 ) )`